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

Theorem txtube 21362
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 481 . . . . . . 7 ((𝜑𝑥𝑋) → (𝑋 × {𝐴}) ⊆ 𝑈)
4 id 22 . . . . . . . 8 (𝑥𝑋𝑥𝑋)
5 txtube.a . . . . . . . . 9 (𝜑𝐴𝑌)
6 snidg 4182 . . . . . . . . 9 (𝐴𝑌𝐴 ∈ {𝐴})
75, 6syl 17 . . . . . . . 8 (𝜑𝐴 ∈ {𝐴})
8 opelxpi 5113 . . . . . . . 8 ((𝑥𝑋𝐴 ∈ {𝐴}) → ⟨𝑥, 𝐴⟩ ∈ (𝑋 × {𝐴}))
94, 7, 8syl2anr 495 . . . . . . 7 ((𝜑𝑥𝑋) → ⟨𝑥, 𝐴⟩ ∈ (𝑋 × {𝐴}))
103, 9sseldd 3588 . . . . . 6 ((𝜑𝑥𝑋) → ⟨𝑥, 𝐴⟩ ∈ 𝑈)
11 txtube.w . . . . . . . 8 (𝜑𝑈 ∈ (𝑅 ×t 𝑆))
12 txtube.s . . . . . . . . 9 (𝜑𝑆 ∈ Top)
13 eltx 21290 . . . . . . . . 9 ((𝑅 ∈ Comp ∧ 𝑆 ∈ Top) → (𝑈 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦𝑈𝑢𝑅𝑣𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
141, 12, 13syl2anc 692 . . . . . . . 8 (𝜑 → (𝑈 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦𝑈𝑢𝑅𝑣𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
1511, 14mpbid 222 . . . . . . 7 (𝜑 → ∀𝑦𝑈𝑢𝑅𝑣𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈))
1615adantr 481 . . . . . 6 ((𝜑𝑥𝑋) → ∀𝑦𝑈𝑢𝑅𝑣𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈))
17 eleq1 2686 . . . . . . . . 9 (𝑦 = ⟨𝑥, 𝐴⟩ → (𝑦 ∈ (𝑢 × 𝑣) ↔ ⟨𝑥, 𝐴⟩ ∈ (𝑢 × 𝑣)))
1817anbi1d 740 . . . . . . . 8 (𝑦 = ⟨𝑥, 𝐴⟩ → ((𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ (⟨𝑥, 𝐴⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
19182rexbidv 3051 . . . . . . 7 (𝑦 = ⟨𝑥, 𝐴⟩ → (∃𝑢𝑅𝑣𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ ∃𝑢𝑅𝑣𝑆 (⟨𝑥, 𝐴⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
2019rspcv 3294 . . . . . 6 (⟨𝑥, 𝐴⟩ ∈ 𝑈 → (∀𝑦𝑈𝑢𝑅𝑣𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) → ∃𝑢𝑅𝑣𝑆 (⟨𝑥, 𝐴⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
2110, 16, 20sylc 65 . . . . 5 ((𝜑𝑥𝑋) → ∃𝑢𝑅𝑣𝑆 (⟨𝑥, 𝐴⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈))
22 opelxp 5111 . . . . . . . . . 10 (⟨𝑥, 𝐴⟩ ∈ (𝑢 × 𝑣) ↔ (𝑥𝑢𝐴𝑣))
2322anbi1i 730 . . . . . . . . 9 ((⟨𝑥, 𝐴⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ ((𝑥𝑢𝐴𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈))
24 anass 680 . . . . . . . . 9 (((𝑥𝑢𝐴𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ (𝑥𝑢 ∧ (𝐴𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
2523, 24bitri 264 . . . . . . . 8 ((⟨𝑥, 𝐴⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ (𝑥𝑢 ∧ (𝐴𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
2625rexbii 3035 . . . . . . 7 (∃𝑣𝑆 (⟨𝑥, 𝐴⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ ∃𝑣𝑆 (𝑥𝑢 ∧ (𝐴𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
27 r19.42v 3085 . . . . . . 7 (∃𝑣𝑆 (𝑥𝑢 ∧ (𝐴𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈)) ↔ (𝑥𝑢 ∧ ∃𝑣𝑆 (𝐴𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
2826, 27bitri 264 . . . . . 6 (∃𝑣𝑆 (⟨𝑥, 𝐴⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ (𝑥𝑢 ∧ ∃𝑣𝑆 (𝐴𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
2928rexbii 3035 . . . . 5 (∃𝑢𝑅𝑣𝑆 (⟨𝑥, 𝐴⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ ∃𝑢𝑅 (𝑥𝑢 ∧ ∃𝑣𝑆 (𝐴𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
3021, 29sylib 208 . . . 4 ((𝜑𝑥𝑋) → ∃𝑢𝑅 (𝑥𝑢 ∧ ∃𝑣𝑆 (𝐴𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
3130ralrimiva 2961 . . 3 (𝜑 → ∀𝑥𝑋𝑢𝑅 (𝑥𝑢 ∧ ∃𝑣𝑆 (𝐴𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈)))
32 txtube.x . . . 4 𝑋 = 𝑅
33 eleq2 2687 . . . . 5 (𝑣 = (𝑓𝑢) → (𝐴𝑣𝐴 ∈ (𝑓𝑢)))
34 xpeq2 5094 . . . . . 6 (𝑣 = (𝑓𝑢) → (𝑢 × 𝑣) = (𝑢 × (𝑓𝑢)))
3534sseq1d 3616 . . . . 5 (𝑣 = (𝑓𝑢) → ((𝑢 × 𝑣) ⊆ 𝑈 ↔ (𝑢 × (𝑓𝑢)) ⊆ 𝑈))
3633, 35anbi12d 746 . . . 4 (𝑣 = (𝑓𝑢) → ((𝐴𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))
3732, 36cmpcovf 21113 . . 3 ((𝑅 ∈ Comp ∧ ∀𝑥𝑋𝑢𝑅 (𝑥𝑢 ∧ ∃𝑣𝑆 (𝐴𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈))) → ∃𝑡 ∈ (𝒫 𝑅 ∩ Fin)(𝑋 = 𝑡 ∧ ∃𝑓(𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈))))
381, 31, 37syl2anc 692 . 2 (𝜑 → ∃𝑡 ∈ (𝒫 𝑅 ∩ Fin)(𝑋 = 𝑡 ∧ ∃𝑓(𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈))))
39 rint0 4487 . . . . . . . . . 10 (ran 𝑓 = ∅ → (𝑌 ran 𝑓) = 𝑌)
4039adantl 482 . . . . . . . . 9 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 = ∅) → (𝑌 ran 𝑓) = 𝑌)
41 txtube.y . . . . . . . . . . . 12 𝑌 = 𝑆
4241topopn 20639 . . . . . . . . . . 11 (𝑆 ∈ Top → 𝑌𝑆)
4312, 42syl 17 . . . . . . . . . 10 (𝜑𝑌𝑆)
4443ad3antrrr 765 . . . . . . . . 9 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 = ∅) → 𝑌𝑆)
4540, 44eqeltrd 2698 . . . . . . . 8 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 = ∅) → (𝑌 ran 𝑓) ∈ 𝑆)
4612ad3antrrr 765 . . . . . . . . . . . . 13 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → 𝑆 ∈ Top)
47 simprrl 803 . . . . . . . . . . . . . . 15 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝑓:𝑡𝑆)
48 frn 6015 . . . . . . . . . . . . . . 15 (𝑓:𝑡𝑆 → ran 𝑓𝑆)
4947, 48syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → ran 𝑓𝑆)
5049adantr 481 . . . . . . . . . . . . 13 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → ran 𝑓𝑆)
51 simpr 477 . . . . . . . . . . . . 13 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → ran 𝑓 ≠ ∅)
52 inss2 3817 . . . . . . . . . . . . . . . 16 (𝒫 𝑅 ∩ Fin) ⊆ Fin
53 simplr 791 . . . . . . . . . . . . . . . 16 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝑡 ∈ (𝒫 𝑅 ∩ Fin))
5452, 53sseldi 3585 . . . . . . . . . . . . . . 15 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝑡 ∈ Fin)
55 ffn 6007 . . . . . . . . . . . . . . . . 17 (𝑓:𝑡𝑆𝑓 Fn 𝑡)
5647, 55syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝑓 Fn 𝑡)
57 dffn4 6083 . . . . . . . . . . . . . . . 16 (𝑓 Fn 𝑡𝑓:𝑡onto→ran 𝑓)
5856, 57sylib 208 . . . . . . . . . . . . . . 15 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝑓:𝑡onto→ran 𝑓)
59 fofi 8203 . . . . . . . . . . . . . . 15 ((𝑡 ∈ Fin ∧ 𝑓:𝑡onto→ran 𝑓) → ran 𝑓 ∈ Fin)
6054, 58, 59syl2anc 692 . . . . . . . . . . . . . 14 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → ran 𝑓 ∈ Fin)
6160adantr 481 . . . . . . . . . . . . 13 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → ran 𝑓 ∈ Fin)
62 fiinopn 20634 . . . . . . . . . . . . . 14 (𝑆 ∈ Top → ((ran 𝑓𝑆 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin) → ran 𝑓𝑆))
6362imp 445 . . . . . . . . . . . . 13 ((𝑆 ∈ Top ∧ (ran 𝑓𝑆 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin)) → ran 𝑓𝑆)
6446, 50, 51, 61, 63syl13anc 1325 . . . . . . . . . . . 12 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → ran 𝑓𝑆)
65 elssuni 4438 . . . . . . . . . . . 12 ( ran 𝑓𝑆 ran 𝑓 𝑆)
6664, 65syl 17 . . . . . . . . . . 11 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → ran 𝑓 𝑆)
6766, 41syl6sseqr 3636 . . . . . . . . . 10 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → ran 𝑓𝑌)
68 sseqin2 3800 . . . . . . . . . 10 ( ran 𝑓𝑌 ↔ (𝑌 ran 𝑓) = ran 𝑓)
6967, 68sylib 208 . . . . . . . . 9 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → (𝑌 ran 𝑓) = ran 𝑓)
7069, 64eqeltrd 2698 . . . . . . . 8 ((((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → (𝑌 ran 𝑓) ∈ 𝑆)
7145, 70pm2.61dane 2877 . . . . . . 7 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → (𝑌 ran 𝑓) ∈ 𝑆)
725ad2antrr 761 . . . . . . . 8 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝐴𝑌)
73 simprrr 804 . . . . . . . . . . 11 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈))
74 simpl 473 . . . . . . . . . . . 12 ((𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈) → 𝐴 ∈ (𝑓𝑢))
7574ralimi 2947 . . . . . . . . . . 11 (∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈) → ∀𝑢𝑡 𝐴 ∈ (𝑓𝑢))
7673, 75syl 17 . . . . . . . . . 10 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → ∀𝑢𝑡 𝐴 ∈ (𝑓𝑢))
77 eliin 4496 . . . . . . . . . . 11 (𝐴𝑌 → (𝐴 𝑢𝑡 (𝑓𝑢) ↔ ∀𝑢𝑡 𝐴 ∈ (𝑓𝑢)))
7872, 77syl 17 . . . . . . . . . 10 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → (𝐴 𝑢𝑡 (𝑓𝑢) ↔ ∀𝑢𝑡 𝐴 ∈ (𝑓𝑢)))
7976, 78mpbird 247 . . . . . . . . 9 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝐴 𝑢𝑡 (𝑓𝑢))
80 fniinfv 6219 . . . . . . . . . 10 (𝑓 Fn 𝑡 𝑢𝑡 (𝑓𝑢) = ran 𝑓)
8156, 80syl 17 . . . . . . . . 9 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝑢𝑡 (𝑓𝑢) = ran 𝑓)
8279, 81eleqtrd 2700 . . . . . . . 8 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝐴 ran 𝑓)
8372, 82elind 3781 . . . . . . 7 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝐴 ∈ (𝑌 ran 𝑓))
84 simprl 793 . . . . . . . . . . 11 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝑋 = 𝑡)
85 uniiun 4544 . . . . . . . . . . 11 𝑡 = 𝑢𝑡 𝑢
8684, 85syl6eq 2671 . . . . . . . . . 10 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝑋 = 𝑢𝑡 𝑢)
8786xpeq1d 5103 . . . . . . . . 9 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → (𝑋 × (𝑌 ran 𝑓)) = ( 𝑢𝑡 𝑢 × (𝑌 ran 𝑓)))
88 xpiundir 5140 . . . . . . . . 9 ( 𝑢𝑡 𝑢 × (𝑌 ran 𝑓)) = 𝑢𝑡 (𝑢 × (𝑌 ran 𝑓))
8987, 88syl6eq 2671 . . . . . . . 8 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → (𝑋 × (𝑌 ran 𝑓)) = 𝑢𝑡 (𝑢 × (𝑌 ran 𝑓)))
90 simpr 477 . . . . . . . . . . . 12 ((𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈) → (𝑢 × (𝑓𝑢)) ⊆ 𝑈)
9190ralimi 2947 . . . . . . . . . . 11 (∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈) → ∀𝑢𝑡 (𝑢 × (𝑓𝑢)) ⊆ 𝑈)
9273, 91syl 17 . . . . . . . . . 10 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → ∀𝑢𝑡 (𝑢 × (𝑓𝑢)) ⊆ 𝑈)
93 inss2 3817 . . . . . . . . . . . . 13 (𝑌 ran 𝑓) ⊆ ran 𝑓
9480adantr 481 . . . . . . . . . . . . . 14 ((𝑓 Fn 𝑡𝑢𝑡) → 𝑢𝑡 (𝑓𝑢) = ran 𝑓)
95 iinss2 4543 . . . . . . . . . . . . . . 15 (𝑢𝑡 𝑢𝑡 (𝑓𝑢) ⊆ (𝑓𝑢))
9695adantl 482 . . . . . . . . . . . . . 14 ((𝑓 Fn 𝑡𝑢𝑡) → 𝑢𝑡 (𝑓𝑢) ⊆ (𝑓𝑢))
9794, 96eqsstr3d 3624 . . . . . . . . . . . . 13 ((𝑓 Fn 𝑡𝑢𝑡) → ran 𝑓 ⊆ (𝑓𝑢))
9893, 97syl5ss 3598 . . . . . . . . . . . 12 ((𝑓 Fn 𝑡𝑢𝑡) → (𝑌 ran 𝑓) ⊆ (𝑓𝑢))
99 xpss2 5195 . . . . . . . . . . . 12 ((𝑌 ran 𝑓) ⊆ (𝑓𝑢) → (𝑢 × (𝑌 ran 𝑓)) ⊆ (𝑢 × (𝑓𝑢)))
100 sstr2 3594 . . . . . . . . . . . 12 ((𝑢 × (𝑌 ran 𝑓)) ⊆ (𝑢 × (𝑓𝑢)) → ((𝑢 × (𝑓𝑢)) ⊆ 𝑈 → (𝑢 × (𝑌 ran 𝑓)) ⊆ 𝑈))
10198, 99, 1003syl 18 . . . . . . . . . . 11 ((𝑓 Fn 𝑡𝑢𝑡) → ((𝑢 × (𝑓𝑢)) ⊆ 𝑈 → (𝑢 × (𝑌 ran 𝑓)) ⊆ 𝑈))
102101ralimdva 2957 . . . . . . . . . 10 (𝑓 Fn 𝑡 → (∀𝑢𝑡 (𝑢 × (𝑓𝑢)) ⊆ 𝑈 → ∀𝑢𝑡 (𝑢 × (𝑌 ran 𝑓)) ⊆ 𝑈))
10356, 92, 102sylc 65 . . . . . . . . 9 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → ∀𝑢𝑡 (𝑢 × (𝑌 ran 𝑓)) ⊆ 𝑈)
104 iunss 4532 . . . . . . . . 9 ( 𝑢𝑡 (𝑢 × (𝑌 ran 𝑓)) ⊆ 𝑈 ↔ ∀𝑢𝑡 (𝑢 × (𝑌 ran 𝑓)) ⊆ 𝑈)
105103, 104sylibr 224 . . . . . . . 8 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → 𝑢𝑡 (𝑢 × (𝑌 ran 𝑓)) ⊆ 𝑈)
10689, 105eqsstrd 3623 . . . . . . 7 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → (𝑋 × (𝑌 ran 𝑓)) ⊆ 𝑈)
107 eleq2 2687 . . . . . . . . 9 (𝑢 = (𝑌 ran 𝑓) → (𝐴𝑢𝐴 ∈ (𝑌 ran 𝑓)))
108 xpeq2 5094 . . . . . . . . . 10 (𝑢 = (𝑌 ran 𝑓) → (𝑋 × 𝑢) = (𝑋 × (𝑌 ran 𝑓)))
109108sseq1d 3616 . . . . . . . . 9 (𝑢 = (𝑌 ran 𝑓) → ((𝑋 × 𝑢) ⊆ 𝑈 ↔ (𝑋 × (𝑌 ran 𝑓)) ⊆ 𝑈))
110107, 109anbi12d 746 . . . . . . . 8 (𝑢 = (𝑌 ran 𝑓) → ((𝐴𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈) ↔ (𝐴 ∈ (𝑌 ran 𝑓) ∧ (𝑋 × (𝑌 ran 𝑓)) ⊆ 𝑈)))
111110rspcev 3298 . . . . . . 7 (((𝑌 ran 𝑓) ∈ 𝑆 ∧ (𝐴 ∈ (𝑌 ran 𝑓) ∧ (𝑋 × (𝑌 ran 𝑓)) ⊆ 𝑈)) → ∃𝑢𝑆 (𝐴𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈))
11271, 83, 106, 111syl12anc 1321 . . . . . 6 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = 𝑡 ∧ (𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)))) → ∃𝑢𝑆 (𝐴𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈))
113112expr 642 . . . . 5 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ 𝑋 = 𝑡) → ((𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)) → ∃𝑢𝑆 (𝐴𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈)))
114113exlimdv 1858 . . . 4 (((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ 𝑋 = 𝑡) → (∃𝑓(𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈)) → ∃𝑢𝑆 (𝐴𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈)))
115114expimpd 628 . . 3 ((𝜑𝑡 ∈ (𝒫 𝑅 ∩ Fin)) → ((𝑋 = 𝑡 ∧ ∃𝑓(𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈))) → ∃𝑢𝑆 (𝐴𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈)))
116115rexlimdva 3025 . 2 (𝜑 → (∃𝑡 ∈ (𝒫 𝑅 ∩ Fin)(𝑋 = 𝑡 ∧ ∃𝑓(𝑓:𝑡𝑆 ∧ ∀𝑢𝑡 (𝐴 ∈ (𝑓𝑢) ∧ (𝑢 × (𝑓𝑢)) ⊆ 𝑈))) → ∃𝑢𝑆 (𝐴𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈)))
11738, 116mpd 15 1 (𝜑 → ∃𝑢𝑆 (𝐴𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wex 1701  wcel 1987  wne 2790  wral 2907  wrex 2908  cin 3558  wss 3559  c0 3896  𝒫 cpw 4135  {csn 4153  cop 4159   cuni 4407   cint 4445   ciun 4490   ciin 4491   × cxp 5077  ran crn 5080   Fn wfn 5847  wf 5848  ontowfo 5850  cfv 5852  (class class class)co 6610  Fincfn 7906  Topctop 20626  Compccmp 21108   ×t ctx 21282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-oadd 7516  df-er 7694  df-en 7907  df-dom 7908  df-fin 7910  df-topgen 16032  df-top 20627  df-cmp 21109  df-tx 21284
This theorem is referenced by:  txcmplem1  21363  xkoinjcn  21409  cvmlift2lem12  31031
  Copyright terms: Public domain W3C validator