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

Theorem txconn 23415
Description: The topological product of two connected spaces is connected. (Contributed by Mario Carneiro, 29-Mar-2015.)
Assertion
Ref Expression
txconn ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) β†’ (𝑅 Γ—t 𝑆) ∈ Conn)

Proof of Theorem txconn
Dummy variables 𝑀 π‘Ž π‘₯ 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 conntop 23143 . . 3 (𝑅 ∈ Conn β†’ 𝑅 ∈ Top)
2 conntop 23143 . . 3 (𝑆 ∈ Conn β†’ 𝑆 ∈ Top)
3 txtop 23295 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑅 Γ—t 𝑆) ∈ Top)
41, 2, 3syl2an 594 . 2 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) β†’ (𝑅 Γ—t 𝑆) ∈ Top)
5 neq0 4346 . . . . . . 7 (Β¬ π‘₯ = βˆ… ↔ βˆƒπ‘§ 𝑧 ∈ π‘₯)
6 simplr 765 . . . . . . . . . . . 12 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ 𝑧 ∈ π‘₯) β†’ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆))))
76elin1d 4199 . . . . . . . . . . 11 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ 𝑧 ∈ π‘₯) β†’ π‘₯ ∈ (𝑅 Γ—t 𝑆))
8 elssuni 4942 . . . . . . . . . . 11 (π‘₯ ∈ (𝑅 Γ—t 𝑆) β†’ π‘₯ βŠ† βˆͺ (𝑅 Γ—t 𝑆))
97, 8syl 17 . . . . . . . . . 10 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ 𝑧 ∈ π‘₯) β†’ π‘₯ βŠ† βˆͺ (𝑅 Γ—t 𝑆))
10 simprr 769 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))
11 simplll 771 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑅 ∈ Conn)
1211, 1syl 17 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑅 ∈ Top)
13 simpllr 772 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑆 ∈ Conn)
1413, 2syl 17 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑆 ∈ Top)
15 eqid 2730 . . . . . . . . . . . . . . . . 17 βˆͺ 𝑅 = βˆͺ 𝑅
16 eqid 2730 . . . . . . . . . . . . . . . . 17 βˆͺ 𝑆 = βˆͺ 𝑆
1715, 16txuni 23318 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) = βˆͺ (𝑅 Γ—t 𝑆))
1812, 14, 17syl2anc 582 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) = βˆͺ (𝑅 Γ—t 𝑆))
1910, 18eleqtrrd 2834 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑀 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))
20 1st2nd2 8018 . . . . . . . . . . . . . 14 (𝑀 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) β†’ 𝑀 = ⟨(1st β€˜π‘€), (2nd β€˜π‘€)⟩)
2119, 20syl 17 . . . . . . . . . . . . 13 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑀 = ⟨(1st β€˜π‘€), (2nd β€˜π‘€)⟩)
22 xp2nd 8012 . . . . . . . . . . . . . . . 16 (𝑀 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) β†’ (2nd β€˜π‘€) ∈ βˆͺ 𝑆)
2319, 22syl 17 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (2nd β€˜π‘€) ∈ βˆͺ 𝑆)
24 eqid 2730 . . . . . . . . . . . . . . . . . 18 (π‘Ž ∈ βˆͺ 𝑆 ↦ ⟨(1st β€˜π‘€), π‘ŽβŸ©) = (π‘Ž ∈ βˆͺ 𝑆 ↦ ⟨(1st β€˜π‘€), π‘ŽβŸ©)
2524mptpreima 6238 . . . . . . . . . . . . . . . . 17 (β—‘(π‘Ž ∈ βˆͺ 𝑆 ↦ ⟨(1st β€˜π‘€), π‘ŽβŸ©) β€œ π‘₯) = {π‘Ž ∈ βˆͺ 𝑆 ∣ ⟨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯}
26 toptopon2 22642 . . . . . . . . . . . . . . . . . . . 20 (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOnβ€˜βˆͺ 𝑆))
2714, 26sylib 217 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑆 ∈ (TopOnβ€˜βˆͺ 𝑆))
28 toptopon2 22642 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOnβ€˜βˆͺ 𝑅))
2912, 28sylib 217 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑅 ∈ (TopOnβ€˜βˆͺ 𝑅))
30 xp1st 8011 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) β†’ (1st β€˜π‘€) ∈ βˆͺ 𝑅)
3119, 30syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (1st β€˜π‘€) ∈ βˆͺ 𝑅)
3227, 29, 31cnmptc 23388 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (π‘Ž ∈ βˆͺ 𝑆 ↦ (1st β€˜π‘€)) ∈ (𝑆 Cn 𝑅))
3327cnmptid 23387 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (π‘Ž ∈ βˆͺ 𝑆 ↦ π‘Ž) ∈ (𝑆 Cn 𝑆))
3427, 32, 33cnmpt1t 23391 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (π‘Ž ∈ βˆͺ 𝑆 ↦ ⟨(1st β€˜π‘€), π‘ŽβŸ©) ∈ (𝑆 Cn (𝑅 Γ—t 𝑆)))
35 simplr 765 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆))))
3635elin1d 4199 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ π‘₯ ∈ (𝑅 Γ—t 𝑆))
37 cnima 22991 . . . . . . . . . . . . . . . . . 18 (((π‘Ž ∈ βˆͺ 𝑆 ↦ ⟨(1st β€˜π‘€), π‘ŽβŸ©) ∈ (𝑆 Cn (𝑅 Γ—t 𝑆)) ∧ π‘₯ ∈ (𝑅 Γ—t 𝑆)) β†’ (β—‘(π‘Ž ∈ βˆͺ 𝑆 ↦ ⟨(1st β€˜π‘€), π‘ŽβŸ©) β€œ π‘₯) ∈ 𝑆)
3834, 36, 37syl2anc 582 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (β—‘(π‘Ž ∈ βˆͺ 𝑆 ↦ ⟨(1st β€˜π‘€), π‘ŽβŸ©) β€œ π‘₯) ∈ 𝑆)
3925, 38eqeltrrid 2836 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ {π‘Ž ∈ βˆͺ 𝑆 ∣ ⟨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯} ∈ 𝑆)
40 simprl 767 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑧 ∈ π‘₯)
41 elunii 4914 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 ∈ π‘₯ ∧ π‘₯ ∈ (𝑅 Γ—t 𝑆)) β†’ 𝑧 ∈ βˆͺ (𝑅 Γ—t 𝑆))
4240, 36, 41syl2anc 582 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑧 ∈ βˆͺ (𝑅 Γ—t 𝑆))
4342, 18eleqtrrd 2834 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑧 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))
44 xp2nd 8012 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) β†’ (2nd β€˜π‘§) ∈ βˆͺ 𝑆)
4543, 44syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (2nd β€˜π‘§) ∈ βˆͺ 𝑆)
46 eqid 2730 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘Ž ∈ βˆͺ 𝑅 ↦ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩) = (π‘Ž ∈ βˆͺ 𝑅 ↦ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩)
4746mptpreima 6238 . . . . . . . . . . . . . . . . . . . . . 22 (β—‘(π‘Ž ∈ βˆͺ 𝑅 ↦ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩) β€œ π‘₯) = {π‘Ž ∈ βˆͺ 𝑅 ∣ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯}
4829cnmptid 23387 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (π‘Ž ∈ βˆͺ 𝑅 ↦ π‘Ž) ∈ (𝑅 Cn 𝑅))
4929, 27, 45cnmptc 23388 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (π‘Ž ∈ βˆͺ 𝑅 ↦ (2nd β€˜π‘§)) ∈ (𝑅 Cn 𝑆))
5029, 48, 49cnmpt1t 23391 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (π‘Ž ∈ βˆͺ 𝑅 ↦ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩) ∈ (𝑅 Cn (𝑅 Γ—t 𝑆)))
51 cnima 22991 . . . . . . . . . . . . . . . . . . . . . . 23 (((π‘Ž ∈ βˆͺ 𝑅 ↦ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩) ∈ (𝑅 Cn (𝑅 Γ—t 𝑆)) ∧ π‘₯ ∈ (𝑅 Γ—t 𝑆)) β†’ (β—‘(π‘Ž ∈ βˆͺ 𝑅 ↦ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩) β€œ π‘₯) ∈ 𝑅)
5250, 36, 51syl2anc 582 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (β—‘(π‘Ž ∈ βˆͺ 𝑅 ↦ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩) β€œ π‘₯) ∈ 𝑅)
5347, 52eqeltrrid 2836 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ {π‘Ž ∈ βˆͺ 𝑅 ∣ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯} ∈ 𝑅)
54 xp1st 8011 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) β†’ (1st β€˜π‘§) ∈ βˆͺ 𝑅)
5543, 54syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (1st β€˜π‘§) ∈ βˆͺ 𝑅)
56 1st2nd2 8018 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) β†’ 𝑧 = ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩)
5743, 56syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑧 = ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩)
5857, 40eqeltrrd 2832 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩ ∈ π‘₯)
59 opeq1 4874 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘Ž = (1st β€˜π‘§) β†’ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ = ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩)
6059eleq1d 2816 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘Ž = (1st β€˜π‘§) β†’ (βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯ ↔ ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩ ∈ π‘₯))
6160rspcev 3613 . . . . . . . . . . . . . . . . . . . . . . 23 (((1st β€˜π‘§) ∈ βˆͺ 𝑅 ∧ ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩ ∈ π‘₯) β†’ βˆƒπ‘Ž ∈ βˆͺ π‘…βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯)
6255, 58, 61syl2anc 582 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ βˆƒπ‘Ž ∈ βˆͺ π‘…βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯)
63 rabn0 4386 . . . . . . . . . . . . . . . . . . . . . 22 ({π‘Ž ∈ βˆͺ 𝑅 ∣ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯} β‰  βˆ… ↔ βˆƒπ‘Ž ∈ βˆͺ π‘…βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯)
6462, 63sylibr 233 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ {π‘Ž ∈ βˆͺ 𝑅 ∣ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯} β‰  βˆ…)
6535elin2d 4200 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ π‘₯ ∈ (Clsdβ€˜(𝑅 Γ—t 𝑆)))
66 cnclima 22994 . . . . . . . . . . . . . . . . . . . . . . 23 (((π‘Ž ∈ βˆͺ 𝑅 ↦ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩) ∈ (𝑅 Cn (𝑅 Γ—t 𝑆)) ∧ π‘₯ ∈ (Clsdβ€˜(𝑅 Γ—t 𝑆))) β†’ (β—‘(π‘Ž ∈ βˆͺ 𝑅 ↦ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩) β€œ π‘₯) ∈ (Clsdβ€˜π‘…))
6750, 65, 66syl2anc 582 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (β—‘(π‘Ž ∈ βˆͺ 𝑅 ↦ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩) β€œ π‘₯) ∈ (Clsdβ€˜π‘…))
6847, 67eqeltrrid 2836 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ {π‘Ž ∈ βˆͺ 𝑅 ∣ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯} ∈ (Clsdβ€˜π‘…))
6915, 11, 53, 64, 68connclo 23141 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ {π‘Ž ∈ βˆͺ 𝑅 ∣ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯} = βˆͺ 𝑅)
7031, 69eleqtrrd 2834 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (1st β€˜π‘€) ∈ {π‘Ž ∈ βˆͺ 𝑅 ∣ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯})
71 opeq1 4874 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Ž = (1st β€˜π‘€) β†’ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ = ⟨(1st β€˜π‘€), (2nd β€˜π‘§)⟩)
7271eleq1d 2816 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž = (1st β€˜π‘€) β†’ (βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯ ↔ ⟨(1st β€˜π‘€), (2nd β€˜π‘§)⟩ ∈ π‘₯))
7372elrab 3684 . . . . . . . . . . . . . . . . . . . 20 ((1st β€˜π‘€) ∈ {π‘Ž ∈ βˆͺ 𝑅 ∣ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯} ↔ ((1st β€˜π‘€) ∈ βˆͺ 𝑅 ∧ ⟨(1st β€˜π‘€), (2nd β€˜π‘§)⟩ ∈ π‘₯))
7473simprbi 495 . . . . . . . . . . . . . . . . . . 19 ((1st β€˜π‘€) ∈ {π‘Ž ∈ βˆͺ 𝑅 ∣ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯} β†’ ⟨(1st β€˜π‘€), (2nd β€˜π‘§)⟩ ∈ π‘₯)
7570, 74syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ ⟨(1st β€˜π‘€), (2nd β€˜π‘§)⟩ ∈ π‘₯)
76 opeq2 4875 . . . . . . . . . . . . . . . . . . . 20 (π‘Ž = (2nd β€˜π‘§) β†’ ⟨(1st β€˜π‘€), π‘ŽβŸ© = ⟨(1st β€˜π‘€), (2nd β€˜π‘§)⟩)
7776eleq1d 2816 . . . . . . . . . . . . . . . . . . 19 (π‘Ž = (2nd β€˜π‘§) β†’ (⟨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯ ↔ ⟨(1st β€˜π‘€), (2nd β€˜π‘§)⟩ ∈ π‘₯))
7877rspcev 3613 . . . . . . . . . . . . . . . . . 18 (((2nd β€˜π‘§) ∈ βˆͺ 𝑆 ∧ ⟨(1st β€˜π‘€), (2nd β€˜π‘§)⟩ ∈ π‘₯) β†’ βˆƒπ‘Ž ∈ βˆͺ π‘†βŸ¨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯)
7945, 75, 78syl2anc 582 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ βˆƒπ‘Ž ∈ βˆͺ π‘†βŸ¨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯)
80 rabn0 4386 . . . . . . . . . . . . . . . . 17 ({π‘Ž ∈ βˆͺ 𝑆 ∣ ⟨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯} β‰  βˆ… ↔ βˆƒπ‘Ž ∈ βˆͺ π‘†βŸ¨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯)
8179, 80sylibr 233 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ {π‘Ž ∈ βˆͺ 𝑆 ∣ ⟨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯} β‰  βˆ…)
82 cnclima 22994 . . . . . . . . . . . . . . . . . 18 (((π‘Ž ∈ βˆͺ 𝑆 ↦ ⟨(1st β€˜π‘€), π‘ŽβŸ©) ∈ (𝑆 Cn (𝑅 Γ—t 𝑆)) ∧ π‘₯ ∈ (Clsdβ€˜(𝑅 Γ—t 𝑆))) β†’ (β—‘(π‘Ž ∈ βˆͺ 𝑆 ↦ ⟨(1st β€˜π‘€), π‘ŽβŸ©) β€œ π‘₯) ∈ (Clsdβ€˜π‘†))
8334, 65, 82syl2anc 582 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (β—‘(π‘Ž ∈ βˆͺ 𝑆 ↦ ⟨(1st β€˜π‘€), π‘ŽβŸ©) β€œ π‘₯) ∈ (Clsdβ€˜π‘†))
8425, 83eqeltrrid 2836 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ {π‘Ž ∈ βˆͺ 𝑆 ∣ ⟨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯} ∈ (Clsdβ€˜π‘†))
8516, 13, 39, 81, 84connclo 23141 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ {π‘Ž ∈ βˆͺ 𝑆 ∣ ⟨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯} = βˆͺ 𝑆)
8623, 85eleqtrrd 2834 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (2nd β€˜π‘€) ∈ {π‘Ž ∈ βˆͺ 𝑆 ∣ ⟨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯})
87 opeq2 4875 . . . . . . . . . . . . . . . . 17 (π‘Ž = (2nd β€˜π‘€) β†’ ⟨(1st β€˜π‘€), π‘ŽβŸ© = ⟨(1st β€˜π‘€), (2nd β€˜π‘€)⟩)
8887eleq1d 2816 . . . . . . . . . . . . . . . 16 (π‘Ž = (2nd β€˜π‘€) β†’ (⟨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯ ↔ ⟨(1st β€˜π‘€), (2nd β€˜π‘€)⟩ ∈ π‘₯))
8988elrab 3684 . . . . . . . . . . . . . . 15 ((2nd β€˜π‘€) ∈ {π‘Ž ∈ βˆͺ 𝑆 ∣ ⟨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯} ↔ ((2nd β€˜π‘€) ∈ βˆͺ 𝑆 ∧ ⟨(1st β€˜π‘€), (2nd β€˜π‘€)⟩ ∈ π‘₯))
9089simprbi 495 . . . . . . . . . . . . . 14 ((2nd β€˜π‘€) ∈ {π‘Ž ∈ βˆͺ 𝑆 ∣ ⟨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯} β†’ ⟨(1st β€˜π‘€), (2nd β€˜π‘€)⟩ ∈ π‘₯)
9186, 90syl 17 . . . . . . . . . . . . 13 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ ⟨(1st β€˜π‘€), (2nd β€˜π‘€)⟩ ∈ π‘₯)
9221, 91eqeltrd 2831 . . . . . . . . . . . 12 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑀 ∈ π‘₯)
9392expr 455 . . . . . . . . . . 11 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ 𝑧 ∈ π‘₯) β†’ (𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆) β†’ 𝑀 ∈ π‘₯))
9493ssrdv 3989 . . . . . . . . . 10 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ 𝑧 ∈ π‘₯) β†’ βˆͺ (𝑅 Γ—t 𝑆) βŠ† π‘₯)
959, 94eqssd 4000 . . . . . . . . 9 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ 𝑧 ∈ π‘₯) β†’ π‘₯ = βˆͺ (𝑅 Γ—t 𝑆))
9695ex 411 . . . . . . . 8 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) β†’ (𝑧 ∈ π‘₯ β†’ π‘₯ = βˆͺ (𝑅 Γ—t 𝑆)))
9796exlimdv 1934 . . . . . . 7 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) β†’ (βˆƒπ‘§ 𝑧 ∈ π‘₯ β†’ π‘₯ = βˆͺ (𝑅 Γ—t 𝑆)))
985, 97biimtrid 241 . . . . . 6 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) β†’ (Β¬ π‘₯ = βˆ… β†’ π‘₯ = βˆͺ (𝑅 Γ—t 𝑆)))
9998orrd 859 . . . . 5 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) β†’ (π‘₯ = βˆ… ∨ π‘₯ = βˆͺ (𝑅 Γ—t 𝑆)))
10099ex 411 . . . 4 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) β†’ (π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆))) β†’ (π‘₯ = βˆ… ∨ π‘₯ = βˆͺ (𝑅 Γ—t 𝑆))))
101 vex 3476 . . . . 5 π‘₯ ∈ V
102101elpr 4652 . . . 4 (π‘₯ ∈ {βˆ…, βˆͺ (𝑅 Γ—t 𝑆)} ↔ (π‘₯ = βˆ… ∨ π‘₯ = βˆͺ (𝑅 Γ—t 𝑆)))
103100, 102imbitrrdi 251 . . 3 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) β†’ (π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆))) β†’ π‘₯ ∈ {βˆ…, βˆͺ (𝑅 Γ—t 𝑆)}))
104103ssrdv 3989 . 2 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) β†’ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆))) βŠ† {βˆ…, βˆͺ (𝑅 Γ—t 𝑆)})
105 eqid 2730 . . 3 βˆͺ (𝑅 Γ—t 𝑆) = βˆͺ (𝑅 Γ—t 𝑆)
106105isconn2 23140 . 2 ((𝑅 Γ—t 𝑆) ∈ Conn ↔ ((𝑅 Γ—t 𝑆) ∈ Top ∧ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆))) βŠ† {βˆ…, βˆͺ (𝑅 Γ—t 𝑆)}))
1074, 104, 106sylanbrc 581 1 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) β†’ (𝑅 Γ—t 𝑆) ∈ Conn)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 394   ∨ wo 843   = wceq 1539  βˆƒwex 1779   ∈ wcel 2104   β‰  wne 2938  βˆƒwrex 3068  {crab 3430   ∩ cin 3948   βŠ† wss 3949  βˆ…c0 4323  {cpr 4631  βŸ¨cop 4635  βˆͺ cuni 4909   ↦ cmpt 5232   Γ— cxp 5675  β—‘ccnv 5676   β€œ cima 5680  β€˜cfv 6544  (class class class)co 7413  1st c1st 7977  2nd c2nd 7978  Topctop 22617  TopOnctopon 22634  Clsdccld 22742   Cn ccn 22950  Conncconn 23137   Γ—t ctx 23286
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7729
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7416  df-oprab 7417  df-mpo 7418  df-1st 7979  df-2nd 7980  df-map 8826  df-topgen 17395  df-top 22618  df-topon 22635  df-bases 22671  df-cld 22745  df-cn 22953  df-cnp 22954  df-conn 23138  df-tx 23288
This theorem is referenced by:  cvmlift2lem9  34598  cvmlift2lem13  34602
  Copyright terms: Public domain W3C validator