MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  txtube Structured version   Visualization version   GIF version

Theorem txtube 21637
Description: The "tube lemma". If 𝑋 is compact and there is an open set 𝑈 containing the line 𝑋 × {𝐴}, then there is a "tube" 𝑋 × 𝑢 for some neighborhood 𝑢 of 𝐴 which is entirely contained within 𝑈. (Contributed by Mario Carneiro, 21-Mar-2015.)
Hypotheses
Ref Expression
txtube.x 𝑋 = 𝑅
txtube.y 𝑌 = 𝑆
txtube.r (𝜑𝑅 ∈ Comp)
txtube.s (𝜑𝑆 ∈ Top)
txtube.w (𝜑𝑈 ∈ (𝑅 ×t 𝑆))
txtube.u (𝜑 → (𝑋 × {𝐴}) ⊆ 𝑈)
txtube.a (𝜑𝐴𝑌)
Assertion
Ref Expression
txtube (𝜑 → ∃𝑢𝑆 (𝐴𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈))
Distinct variable groups:   𝑢,𝐴   𝑢,𝑅   𝑢,𝑆   𝑢,𝑌   𝜑,𝑢   𝑢,𝑈   𝑢,𝑋

Proof of Theorem txtube
Dummy variables 𝑡 𝑓 𝑣 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 txtube.r . . 3 (𝜑𝑅 ∈ Comp)
2 txtube.u . . . . . . . 8 (𝜑 → (𝑋 × {𝐴}) ⊆ 𝑈)
32adantr 472 . . . . . . 7 ((𝜑𝑥𝑋) → (𝑋 × {𝐴}) ⊆ 𝑈)
4 id 22 . . . . . . . 8 (𝑥𝑋𝑥𝑋)
5 txtube.a . . . . . . . . 9 (𝜑𝐴𝑌)
6 snidg 4343 . . . . . . . . 9 (𝐴𝑌𝐴 ∈ {𝐴})
75, 6syl 17 . . . . . . . 8 (𝜑𝐴 ∈ {𝐴})
8 opelxpi 5297 . . . . . . . 8 ((𝑥𝑋𝐴 ∈ {𝐴}) → ⟨𝑥, 𝐴⟩ ∈ (𝑋 × {𝐴}))
94, 7, 8syl2anr 496 . . . . . . 7 ((𝜑𝑥𝑋) → ⟨𝑥, 𝐴⟩ ∈ (𝑋 × {𝐴}))
103, 9sseldd 3737 . . . . . 6 ((𝜑𝑥𝑋) → ⟨𝑥, 𝐴⟩ ∈ 𝑈)
11 txtube.w . . . . . . . 8 (𝜑𝑈 ∈ (𝑅 ×t 𝑆))
12 txtube.s . . . . . . . . 9 (𝜑𝑆 ∈ Top)
13 eltx 21565 . . . . . . . . 9 ((𝑅 ∈ Comp ∧ 𝑆 ∈ Top) → (𝑈 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦𝑈𝑢𝑅𝑣𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
141, 12, 13syl2anc 696 . . . . . . . 8 (𝜑 → (𝑈 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦𝑈𝑢𝑅𝑣𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
1511, 14mpbid 222 . . . . . . 7 (𝜑 → ∀𝑦𝑈𝑢𝑅𝑣𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈))
1615adantr 472 . . . . . 6 ((𝜑𝑥𝑋) → ∀𝑦𝑈𝑢𝑅𝑣𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈))
17 eleq1 2819 . . . . . . . . 9 (𝑦 = ⟨𝑥, 𝐴⟩ → (𝑦 ∈ (𝑢 × 𝑣) ↔ ⟨𝑥, 𝐴⟩ ∈ (𝑢 × 𝑣)))
1817anbi1d 743 . . . . . . . 8 (𝑦 = ⟨𝑥, 𝐴⟩ → ((𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ (⟨𝑥, 𝐴⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
19182rexbidv 3187 . . . . . . 7 (𝑦 = ⟨𝑥, 𝐴⟩ → (∃𝑢𝑅𝑣𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ ∃𝑢𝑅𝑣𝑆 (⟨𝑥, 𝐴⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
2019rspcv 3437 . . . . . 6 (⟨𝑥, 𝐴⟩ ∈ 𝑈 → (∀𝑦𝑈𝑢𝑅𝑣𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) → ∃𝑢𝑅𝑣𝑆 (⟨𝑥, 𝐴⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
2110, 16, 20sylc 65 . . . . 5 ((𝜑𝑥𝑋) → ∃𝑢𝑅𝑣𝑆 (⟨𝑥, 𝐴⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈))
22 opelxp 5295 . . . . . . . . . 10 (⟨𝑥, 𝐴⟩ ∈ (𝑢 × 𝑣) ↔ (𝑥𝑢𝐴𝑣))
2322anbi1i 733 . . . . . . . . 9 ((⟨𝑥, 𝐴⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ ((𝑥𝑢𝐴𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈))
24 anass 684 . . . . . . . . 9 (((𝑥𝑢𝐴𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ (𝑥𝑢 ∧ (𝐴𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
2523, 24bitri 264 . . . . . . . 8 ((⟨𝑥, 𝐴⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ (𝑥𝑢 ∧ (𝐴𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
2625rexbii 3171 . . . . . . 7 (∃𝑣𝑆 (⟨𝑥, 𝐴⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ ∃𝑣𝑆 (𝑥𝑢 ∧ (𝐴𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
27 r19.42v 3222 . . . . . . 7 (∃𝑣𝑆 (𝑥𝑢 ∧ (𝐴𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈)) ↔ (𝑥𝑢 ∧ ∃𝑣𝑆 (𝐴𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
2826, 27bitri 264 . . . . . 6 (∃𝑣𝑆 (⟨𝑥, 𝐴⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ (𝑥𝑢 ∧ ∃𝑣𝑆 (𝐴𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
2928rexbii 3171 . . . . 5 (∃𝑢𝑅𝑣𝑆 (⟨𝑥, 𝐴⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ ∃𝑢𝑅 (𝑥𝑢 ∧ ∃𝑣𝑆 (𝐴𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
3021, 29sylib 208 . . . 4 ((𝜑𝑥𝑋) → ∃𝑢𝑅 (𝑥𝑢 ∧ ∃𝑣𝑆 (𝐴𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
3130ralrimiva 3096 . . 3 (𝜑 → ∀𝑥𝑋𝑢𝑅 (𝑥𝑢 ∧ ∃𝑣𝑆 (𝐴𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
32 txtube.x . . . 4 𝑋 = 𝑅
33 eleq2 2820 . . . . 5 (𝑣 = (𝑓𝑢) → (𝐴𝑣𝐴 ∈ (𝑓𝑢)))
34 xpeq2 5278 . . . . . 6 (𝑣 = (𝑓𝑢) → (𝑢 × 𝑣) = (𝑢 × (𝑓𝑢)))
3534sseq1d 3765 . . . . 5 (𝑣 = (𝑓𝑢) → ((𝑢 × 𝑣) ⊆ 𝑈 ↔ (𝑢 × (𝑓𝑢)) ⊆ 𝑈))
3633, 35anbi12d 749 . . . 4 (𝑣 = (𝑓𝑢) → ((𝐴𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))
3732, 36cmpcovf 21388 . . 3 ((𝑅 ∈ Comp ∧ ∀𝑥𝑋𝑢𝑅 (𝑥𝑢 ∧ ∃𝑣𝑆 (𝐴𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈))) → ∃𝑡 ∈ (𝒫 𝑅 ∩ Fin)(𝑋 = 𝑡 ∧ ∃𝑓(𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈))))
381, 31, 37syl2anc 696 . 2 (𝜑 → ∃𝑡 ∈ (𝒫 𝑅 ∩ Fin)(𝑋 = 𝑡 ∧ ∃𝑓(𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈))))
39 rint0 4661 . . . . . . . . . 10 (ran 𝑓 = ∅ → (𝑌 ran 𝑓) = 𝑌)
4039adantl 473 . . . . . . . . 9 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 = ∅) → (𝑌 ran 𝑓) = 𝑌)
41 txtube.y . . . . . . . . . . . 12 𝑌 = 𝑆
4241topopn 20905 . . . . . . . . . . 11 (𝑆 ∈ Top → 𝑌𝑆)
4312, 42syl 17 . . . . . . . . . 10 (𝜑𝑌𝑆)
4443ad3antrrr 768 . . . . . . . . 9 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 = ∅) → 𝑌𝑆)
4540, 44eqeltrd 2831 . . . . . . . 8 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 = ∅) → (𝑌 ran 𝑓) ∈ 𝑆)
4612ad3antrrr 768 . . . . . . . . . . . . 13 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → 𝑆 ∈ Top)
47 simprrl 823 . . . . . . . . . . . . . . 15 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝑓:𝑡𝑆)
48 frn 6206 . . . . . . . . . . . . . . 15 (𝑓:𝑡𝑆 → ran 𝑓𝑆)
4947, 48syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → ran 𝑓𝑆)
5049adantr 472 . . . . . . . . . . . . 13 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → ran 𝑓𝑆)
51 simpr 479 . . . . . . . . . . . . 13 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → ran 𝑓 ≠ ∅)
52 inss2 3969 . . . . . . . . . . . . . . . 16 (𝒫 𝑅 ∩ Fin) ⊆ Fin
53 simplr 809 . . . . . . . . . . . . . . . 16 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝑡 ∈ (𝒫 𝑅 ∩ Fin))
5452, 53sseldi 3734 . . . . . . . . . . . . . . 15 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝑡 ∈ Fin)
55 ffn 6198 . . . . . . . . . . . . . . . . 17 (𝑓:𝑡𝑆𝑓 Fn 𝑡)
5647, 55syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝑓 Fn 𝑡)
57 dffn4 6274 . . . . . . . . . . . . . . . 16 (𝑓 Fn 𝑡𝑓:𝑡onto→ran 𝑓)
5856, 57sylib 208 . . . . . . . . . . . . . . 15 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝑓:𝑡onto→ran 𝑓)
59 fofi 8409 . . . . . . . . . . . . . . 15 ((𝑡 ∈ Fin ∧ 𝑓:𝑡onto→ran 𝑓) → ran 𝑓 ∈ Fin)
6054, 58, 59syl2anc 696 . . . . . . . . . . . . . 14 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → ran 𝑓 ∈ Fin)
6160adantr 472 . . . . . . . . . . . . 13 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → ran 𝑓 ∈ Fin)
62 fiinopn 20900 . . . . . . . . . . . . . 14 (𝑆 ∈ Top → ((ran 𝑓𝑆 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin) → ran 𝑓𝑆))
6362imp 444 . . . . . . . . . . . . 13 ((𝑆 ∈ Top ∧ (ran 𝑓𝑆 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin)) → ran 𝑓𝑆)
6446, 50, 51, 61, 63syl13anc 1475 . . . . . . . . . . . 12 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → ran 𝑓𝑆)
65 elssuni 4611 . . . . . . . . . . . 12 ( ran 𝑓𝑆 ran 𝑓 𝑆)
6664, 65syl 17 . . . . . . . . . . 11 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → ran 𝑓 𝑆)
6766, 41syl6sseqr 3785 . . . . . . . . . 10 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → ran 𝑓𝑌)
68 sseqin2 3952 . . . . . . . . . 10 ( ran 𝑓𝑌 ↔ (𝑌 ran 𝑓) = ran 𝑓)
6967, 68sylib 208 . . . . . . . . 9 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → (𝑌 ran 𝑓) = ran 𝑓)
7069, 64eqeltrd 2831 . . . . . . . 8 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → (𝑌 ran 𝑓) ∈ 𝑆)
7145, 70pm2.61dane 3011 . . . . . . 7 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → (𝑌 ran 𝑓) ∈ 𝑆)
725ad2antrr 764 . . . . . . . 8 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝐴𝑌)
73 simprrr 824 . . . . . . . . . . 11 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈))
74 simpl 474 . . . . . . . . . . . 12 ((𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈) → 𝐴 ∈ (𝑓𝑢))
7574ralimi 3082 . . . . . . . . . . 11 (∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈) → ∀𝑢𝑡 𝐴 ∈ (𝑓𝑢))
7673, 75syl 17 . . . . . . . . . 10 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → ∀𝑢𝑡 𝐴 ∈ (𝑓𝑢))
77 eliin 4669 . . . . . . . . . . 11 (𝐴𝑌 → (𝐴 𝑢𝑡 (𝑓𝑢) ↔ ∀𝑢𝑡 𝐴 ∈ (𝑓𝑢)))
7872, 77syl 17 . . . . . . . . . 10 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → (𝐴 𝑢𝑡 (𝑓𝑢) ↔ ∀𝑢𝑡 𝐴 ∈ (𝑓𝑢)))
7976, 78mpbird 247 . . . . . . . . 9 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝐴 𝑢𝑡 (𝑓𝑢))
80 fniinfv 6411 . . . . . . . . . 10 (𝑓 Fn 𝑡 𝑢𝑡 (𝑓𝑢) = ran 𝑓)
8156, 80syl 17 . . . . . . . . 9 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝑢𝑡 (𝑓𝑢) = ran 𝑓)
8279, 81eleqtrd 2833 . . . . . . . 8 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝐴 ran 𝑓)
8372, 82elind 3933 . . . . . . 7 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝐴 ∈ (𝑌 ran 𝑓))
84 simprl 811 . . . . . . . . . . 11 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝑋 = 𝑡)
85 uniiun 4717 . . . . . . . . . . 11 𝑡 = 𝑢𝑡 𝑢
8684, 85syl6eq 2802 . . . . . . . . . 10 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝑋 = 𝑢𝑡 𝑢)
8786xpeq1d 5287 . . . . . . . . 9 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → (𝑋 × (𝑌 ran 𝑓)) = ( 𝑢𝑡 𝑢 × (𝑌 ran 𝑓)))
88 xpiundir 5323 . . . . . . . . 9 ( 𝑢𝑡 𝑢 × (𝑌 ran 𝑓)) = 𝑢𝑡 (𝑢 × (𝑌 ran 𝑓))
8987, 88syl6eq 2802 . . . . . . . 8 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → (𝑋 × (𝑌 ran 𝑓)) = 𝑢𝑡 (𝑢 × (𝑌 ran 𝑓)))
90 simpr 479 . . . . . . . . . . . 12 ((𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈) → (𝑢 × (𝑓𝑢)) ⊆ 𝑈)
9190ralimi 3082 . . . . . . . . . . 11 (∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈) → ∀𝑢𝑡 (𝑢 × (𝑓𝑢)) ⊆ 𝑈)
9273, 91syl 17 . . . . . . . . . 10 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → ∀𝑢𝑡 (𝑢 × (𝑓𝑢)) ⊆ 𝑈)
93 inss2 3969 . . . . . . . . . . . . 13 (𝑌 ran 𝑓) ⊆ ran 𝑓
9480adantr 472 . . . . . . . . . . . . . 14 ((𝑓 Fn 𝑡𝑢𝑡) → 𝑢𝑡 (𝑓𝑢) = ran 𝑓)
95 iinss2 4716 . . . . . . . . . . . . . . 15 (𝑢𝑡 𝑢𝑡 (𝑓𝑢) ⊆ (𝑓𝑢))
9695adantl 473 . . . . . . . . . . . . . 14 ((𝑓 Fn 𝑡𝑢𝑡) → 𝑢𝑡 (𝑓𝑢) ⊆ (𝑓𝑢))
9794, 96eqsstr3d 3773 . . . . . . . . . . . . 13 ((𝑓 Fn 𝑡𝑢𝑡) → ran 𝑓 ⊆ (𝑓𝑢))
9893, 97syl5ss 3747 . . . . . . . . . . . 12 ((𝑓 Fn 𝑡𝑢𝑡) → (𝑌 ran 𝑓) ⊆ (𝑓𝑢))
99 xpss2 5277 . . . . . . . . . . . 12 ((𝑌 ran 𝑓) ⊆ (𝑓𝑢) → (𝑢 × (𝑌 ran 𝑓)) ⊆ (𝑢 × (𝑓𝑢)))
100 sstr2 3743 . . . . . . . . . . . 12 ((𝑢 × (𝑌 ran 𝑓)) ⊆ (𝑢 × (𝑓𝑢)) → ((𝑢 × (𝑓𝑢)) ⊆ 𝑈 → (𝑢 × (𝑌 ran 𝑓)) ⊆ 𝑈))
10198, 99, 1003syl 18 . . . . . . . . . . 11 ((𝑓 Fn 𝑡𝑢𝑡) → ((𝑢 × (𝑓𝑢)) ⊆ 𝑈 → (𝑢 × (𝑌 ran 𝑓)) ⊆ 𝑈))
102101ralimdva 3092 . . . . . . . . . 10 (𝑓 Fn 𝑡 → (∀𝑢𝑡 (𝑢 × (𝑓𝑢)) ⊆ 𝑈 → ∀𝑢𝑡 (𝑢 × (𝑌 ran 𝑓)) ⊆ 𝑈))
10356, 92, 102sylc 65 . . . . . . . . 9 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → ∀𝑢𝑡 (𝑢 × (𝑌 ran 𝑓)) ⊆ 𝑈)
104 iunss 4705 . . . . . . . . 9 ( 𝑢𝑡 (𝑢 × (𝑌 ran 𝑓)) ⊆ 𝑈 ↔ ∀𝑢𝑡 (𝑢 × (𝑌 ran 𝑓)) ⊆ 𝑈)
105103, 104sylibr 224 . . . . . . . 8 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝑢𝑡 (𝑢 × (𝑌 ran 𝑓)) ⊆ 𝑈)
10689, 105eqsstrd 3772 . . . . . . 7 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → (𝑋 × (𝑌 ran 𝑓)) ⊆ 𝑈)
107 eleq2 2820 . . . . . . . . 9 (𝑢 = (𝑌 ran 𝑓) → (𝐴𝑢𝐴 ∈ (𝑌 ran 𝑓)))
108 xpeq2 5278 . . . . . . . . . 10 (𝑢 = (𝑌 ran 𝑓) → (𝑋 × 𝑢) = (𝑋 × (𝑌 ran 𝑓)))
109108sseq1d 3765 . . . . . . . . 9 (𝑢 = (𝑌 ran 𝑓) → ((𝑋 × 𝑢) ⊆ 𝑈 ↔ (𝑋 × (𝑌 ran 𝑓)) ⊆ 𝑈))
110107, 109anbi12d 749 . . . . . . . 8 (𝑢 = (𝑌 ran 𝑓) → ((𝐴𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈) ↔ (𝐴 ∈ (𝑌 ran 𝑓) ∧ (𝑋 × (𝑌 ran 𝑓)) ⊆ 𝑈)))
111110rspcev 3441 . . . . . . 7 (((𝑌 ran 𝑓) ∈ 𝑆 ∧ (𝐴 ∈ (𝑌 ran 𝑓) ∧ (𝑋 × (𝑌 ran 𝑓)) ⊆ 𝑈)) → ∃𝑢𝑆 (𝐴𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈))
11271, 83, 106, 111syl12anc 1471 . . . . . 6 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → ∃𝑢𝑆 (𝐴𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈))
113112expr 644 . . . . 5 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ 𝑋 = 𝑡) → ((𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)) → ∃𝑢𝑆 (𝐴𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈)))
114113exlimdv 2002 . . . 4 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ 𝑋 = 𝑡) → (∃𝑓(𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)) → ∃𝑢𝑆 (𝐴𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈)))
115114expimpd 630 . . 3 ((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) → ((𝑋 = 𝑡 ∧ ∃𝑓(𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈))) → ∃𝑢𝑆 (𝐴𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈)))
116115rexlimdva 3161 . 2 (𝜑 → (∃𝑡 ∈ (𝒫 𝑅 ∩ Fin)(𝑋 = 𝑡 ∧ ∃𝑓(𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈))) → ∃𝑢𝑆 (𝐴𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈)))
11738, 116mpd 15 1 (𝜑 → ∃𝑢𝑆 (𝐴𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1624  wex 1845  wcel 2131  wne 2924  wral 3042  wrex 3043  cin 3706  wss 3707  c0 4050  𝒫 cpw 4294  {csn 4313  cop 4319   cuni 4580   cint 4619   ciun 4664   ciin 4665   × cxp 5256  ran crn 5259   Fn wfn 6036  wf 6037  ontowfo 6039  cfv 6041  (class class class)co 6805  Fincfn 8113  Topctop 20892  Compccmp 21383   ×t ctx 21557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-ral 3047  df-rex 3048  df-reu 3049  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-pss 3723  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4581  df-int 4620  df-iun 4666  df-iin 4667  df-br 4797  df-opab 4857  df-mpt 4874  df-tr 4897  df-id 5166  df-eprel 5171  df-po 5179  df-so 5180  df-fr 5217  df-we 5219  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-pred 5833  df-ord 5879  df-on 5880  df-lim 5881  df-suc 5882  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-om 7223  df-1st 7325  df-2nd 7326  df-wrecs 7568  df-recs 7629  df-rdg 7667  df-1o 7721  df-oadd 7725  df-er 7903  df-en 8114  df-dom 8115  df-fin 8117  df-topgen 16298  df-top 20893  df-cmp 21384  df-tx 21559
This theorem is referenced by:  txcmplem1  21638  xkoinjcn  21684  cvmlift2lem12  31595
  Copyright terms: Public domain W3C validator