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

Theorem txconn 23192
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 22920 . . 3 (𝑅 ∈ Conn β†’ 𝑅 ∈ Top)
2 conntop 22920 . . 3 (𝑆 ∈ Conn β†’ 𝑆 ∈ Top)
3 txtop 23072 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑅 Γ—t 𝑆) ∈ Top)
41, 2, 3syl2an 596 . 2 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) β†’ (𝑅 Γ—t 𝑆) ∈ Top)
5 neq0 4345 . . . . . . 7 (Β¬ π‘₯ = βˆ… ↔ βˆƒπ‘§ 𝑧 ∈ π‘₯)
6 simplr 767 . . . . . . . . . . . 12 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ 𝑧 ∈ π‘₯) β†’ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆))))
76elin1d 4198 . . . . . . . . . . 11 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ 𝑧 ∈ π‘₯) β†’ π‘₯ ∈ (𝑅 Γ—t 𝑆))
8 elssuni 4941 . . . . . . . . . . 11 (π‘₯ ∈ (𝑅 Γ—t 𝑆) β†’ π‘₯ βŠ† βˆͺ (𝑅 Γ—t 𝑆))
97, 8syl 17 . . . . . . . . . 10 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ 𝑧 ∈ π‘₯) β†’ π‘₯ βŠ† βˆͺ (𝑅 Γ—t 𝑆))
10 simprr 771 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))
11 simplll 773 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑅 ∈ Conn)
1211, 1syl 17 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑅 ∈ Top)
13 simpllr 774 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑆 ∈ Conn)
1413, 2syl 17 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑆 ∈ Top)
15 eqid 2732 . . . . . . . . . . . . . . . . 17 βˆͺ 𝑅 = βˆͺ 𝑅
16 eqid 2732 . . . . . . . . . . . . . . . . 17 βˆͺ 𝑆 = βˆͺ 𝑆
1715, 16txuni 23095 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) = βˆͺ (𝑅 Γ—t 𝑆))
1812, 14, 17syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) = βˆͺ (𝑅 Γ—t 𝑆))
1910, 18eleqtrrd 2836 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑀 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))
20 1st2nd2 8013 . . . . . . . . . . . . . 14 (𝑀 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) β†’ 𝑀 = ⟨(1st β€˜π‘€), (2nd β€˜π‘€)⟩)
2119, 20syl 17 . . . . . . . . . . . . 13 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑀 = ⟨(1st β€˜π‘€), (2nd β€˜π‘€)⟩)
22 xp2nd 8007 . . . . . . . . . . . . . . . 16 (𝑀 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) β†’ (2nd β€˜π‘€) ∈ βˆͺ 𝑆)
2319, 22syl 17 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (2nd β€˜π‘€) ∈ βˆͺ 𝑆)
24 eqid 2732 . . . . . . . . . . . . . . . . . 18 (π‘Ž ∈ βˆͺ 𝑆 ↦ ⟨(1st β€˜π‘€), π‘ŽβŸ©) = (π‘Ž ∈ βˆͺ 𝑆 ↦ ⟨(1st β€˜π‘€), π‘ŽβŸ©)
2524mptpreima 6237 . . . . . . . . . . . . . . . . 17 (β—‘(π‘Ž ∈ βˆͺ 𝑆 ↦ ⟨(1st β€˜π‘€), π‘ŽβŸ©) β€œ π‘₯) = {π‘Ž ∈ βˆͺ 𝑆 ∣ ⟨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯}
26 toptopon2 22419 . . . . . . . . . . . . . . . . . . . 20 (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOnβ€˜βˆͺ 𝑆))
2714, 26sylib 217 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑆 ∈ (TopOnβ€˜βˆͺ 𝑆))
28 toptopon2 22419 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOnβ€˜βˆͺ 𝑅))
2912, 28sylib 217 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑅 ∈ (TopOnβ€˜βˆͺ 𝑅))
30 xp1st 8006 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) β†’ (1st β€˜π‘€) ∈ βˆͺ 𝑅)
3119, 30syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (1st β€˜π‘€) ∈ βˆͺ 𝑅)
3227, 29, 31cnmptc 23165 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (π‘Ž ∈ βˆͺ 𝑆 ↦ (1st β€˜π‘€)) ∈ (𝑆 Cn 𝑅))
3327cnmptid 23164 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (π‘Ž ∈ βˆͺ 𝑆 ↦ π‘Ž) ∈ (𝑆 Cn 𝑆))
3427, 32, 33cnmpt1t 23168 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (π‘Ž ∈ βˆͺ 𝑆 ↦ ⟨(1st β€˜π‘€), π‘ŽβŸ©) ∈ (𝑆 Cn (𝑅 Γ—t 𝑆)))
35 simplr 767 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆))))
3635elin1d 4198 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ π‘₯ ∈ (𝑅 Γ—t 𝑆))
37 cnima 22768 . . . . . . . . . . . . . . . . . 18 (((π‘Ž ∈ βˆͺ 𝑆 ↦ ⟨(1st β€˜π‘€), π‘ŽβŸ©) ∈ (𝑆 Cn (𝑅 Γ—t 𝑆)) ∧ π‘₯ ∈ (𝑅 Γ—t 𝑆)) β†’ (β—‘(π‘Ž ∈ βˆͺ 𝑆 ↦ ⟨(1st β€˜π‘€), π‘ŽβŸ©) β€œ π‘₯) ∈ 𝑆)
3834, 36, 37syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (β—‘(π‘Ž ∈ βˆͺ 𝑆 ↦ ⟨(1st β€˜π‘€), π‘ŽβŸ©) β€œ π‘₯) ∈ 𝑆)
3925, 38eqeltrrid 2838 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ {π‘Ž ∈ βˆͺ 𝑆 ∣ ⟨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯} ∈ 𝑆)
40 simprl 769 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑧 ∈ π‘₯)
41 elunii 4913 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 ∈ π‘₯ ∧ π‘₯ ∈ (𝑅 Γ—t 𝑆)) β†’ 𝑧 ∈ βˆͺ (𝑅 Γ—t 𝑆))
4240, 36, 41syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑧 ∈ βˆͺ (𝑅 Γ—t 𝑆))
4342, 18eleqtrrd 2836 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑧 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))
44 xp2nd 8007 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) β†’ (2nd β€˜π‘§) ∈ βˆͺ 𝑆)
4543, 44syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (2nd β€˜π‘§) ∈ βˆͺ 𝑆)
46 eqid 2732 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘Ž ∈ βˆͺ 𝑅 ↦ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩) = (π‘Ž ∈ βˆͺ 𝑅 ↦ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩)
4746mptpreima 6237 . . . . . . . . . . . . . . . . . . . . . 22 (β—‘(π‘Ž ∈ βˆͺ 𝑅 ↦ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩) β€œ π‘₯) = {π‘Ž ∈ βˆͺ 𝑅 ∣ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯}
4829cnmptid 23164 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (π‘Ž ∈ βˆͺ 𝑅 ↦ π‘Ž) ∈ (𝑅 Cn 𝑅))
4929, 27, 45cnmptc 23165 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (π‘Ž ∈ βˆͺ 𝑅 ↦ (2nd β€˜π‘§)) ∈ (𝑅 Cn 𝑆))
5029, 48, 49cnmpt1t 23168 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (π‘Ž ∈ βˆͺ 𝑅 ↦ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩) ∈ (𝑅 Cn (𝑅 Γ—t 𝑆)))
51 cnima 22768 . . . . . . . . . . . . . . . . . . . . . . 23 (((π‘Ž ∈ βˆͺ 𝑅 ↦ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩) ∈ (𝑅 Cn (𝑅 Γ—t 𝑆)) ∧ π‘₯ ∈ (𝑅 Γ—t 𝑆)) β†’ (β—‘(π‘Ž ∈ βˆͺ 𝑅 ↦ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩) β€œ π‘₯) ∈ 𝑅)
5250, 36, 51syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (β—‘(π‘Ž ∈ βˆͺ 𝑅 ↦ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩) β€œ π‘₯) ∈ 𝑅)
5347, 52eqeltrrid 2838 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ {π‘Ž ∈ βˆͺ 𝑅 ∣ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯} ∈ 𝑅)
54 xp1st 8006 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) β†’ (1st β€˜π‘§) ∈ βˆͺ 𝑅)
5543, 54syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (1st β€˜π‘§) ∈ βˆͺ 𝑅)
56 1st2nd2 8013 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) β†’ 𝑧 = ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩)
5743, 56syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑧 = ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩)
5857, 40eqeltrrd 2834 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩ ∈ π‘₯)
59 opeq1 4873 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘Ž = (1st β€˜π‘§) β†’ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ = ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩)
6059eleq1d 2818 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘Ž = (1st β€˜π‘§) β†’ (βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯ ↔ ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩ ∈ π‘₯))
6160rspcev 3612 . . . . . . . . . . . . . . . . . . . . . . 23 (((1st β€˜π‘§) ∈ βˆͺ 𝑅 ∧ ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩ ∈ π‘₯) β†’ βˆƒπ‘Ž ∈ βˆͺ π‘…βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯)
6255, 58, 61syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ βˆƒπ‘Ž ∈ βˆͺ π‘…βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯)
63 rabn0 4385 . . . . . . . . . . . . . . . . . . . . . 22 ({π‘Ž ∈ βˆͺ 𝑅 ∣ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯} β‰  βˆ… ↔ βˆƒπ‘Ž ∈ βˆͺ π‘…βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯)
6462, 63sylibr 233 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ {π‘Ž ∈ βˆͺ 𝑅 ∣ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯} β‰  βˆ…)
6535elin2d 4199 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ π‘₯ ∈ (Clsdβ€˜(𝑅 Γ—t 𝑆)))
66 cnclima 22771 . . . . . . . . . . . . . . . . . . . . . . 23 (((π‘Ž ∈ βˆͺ 𝑅 ↦ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩) ∈ (𝑅 Cn (𝑅 Γ—t 𝑆)) ∧ π‘₯ ∈ (Clsdβ€˜(𝑅 Γ—t 𝑆))) β†’ (β—‘(π‘Ž ∈ βˆͺ 𝑅 ↦ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩) β€œ π‘₯) ∈ (Clsdβ€˜π‘…))
6750, 65, 66syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (β—‘(π‘Ž ∈ βˆͺ 𝑅 ↦ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩) β€œ π‘₯) ∈ (Clsdβ€˜π‘…))
6847, 67eqeltrrid 2838 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ {π‘Ž ∈ βˆͺ 𝑅 ∣ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯} ∈ (Clsdβ€˜π‘…))
6915, 11, 53, 64, 68connclo 22918 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ {π‘Ž ∈ βˆͺ 𝑅 ∣ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯} = βˆͺ 𝑅)
7031, 69eleqtrrd 2836 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (1st β€˜π‘€) ∈ {π‘Ž ∈ βˆͺ 𝑅 ∣ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯})
71 opeq1 4873 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Ž = (1st β€˜π‘€) β†’ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ = ⟨(1st β€˜π‘€), (2nd β€˜π‘§)⟩)
7271eleq1d 2818 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž = (1st β€˜π‘€) β†’ (βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯ ↔ ⟨(1st β€˜π‘€), (2nd β€˜π‘§)⟩ ∈ π‘₯))
7372elrab 3683 . . . . . . . . . . . . . . . . . . . 20 ((1st β€˜π‘€) ∈ {π‘Ž ∈ βˆͺ 𝑅 ∣ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯} ↔ ((1st β€˜π‘€) ∈ βˆͺ 𝑅 ∧ ⟨(1st β€˜π‘€), (2nd β€˜π‘§)⟩ ∈ π‘₯))
7473simprbi 497 . . . . . . . . . . . . . . . . . . 19 ((1st β€˜π‘€) ∈ {π‘Ž ∈ βˆͺ 𝑅 ∣ βŸ¨π‘Ž, (2nd β€˜π‘§)⟩ ∈ π‘₯} β†’ ⟨(1st β€˜π‘€), (2nd β€˜π‘§)⟩ ∈ π‘₯)
7570, 74syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ ⟨(1st β€˜π‘€), (2nd β€˜π‘§)⟩ ∈ π‘₯)
76 opeq2 4874 . . . . . . . . . . . . . . . . . . . 20 (π‘Ž = (2nd β€˜π‘§) β†’ ⟨(1st β€˜π‘€), π‘ŽβŸ© = ⟨(1st β€˜π‘€), (2nd β€˜π‘§)⟩)
7776eleq1d 2818 . . . . . . . . . . . . . . . . . . 19 (π‘Ž = (2nd β€˜π‘§) β†’ (⟨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯ ↔ ⟨(1st β€˜π‘€), (2nd β€˜π‘§)⟩ ∈ π‘₯))
7877rspcev 3612 . . . . . . . . . . . . . . . . . 18 (((2nd β€˜π‘§) ∈ βˆͺ 𝑆 ∧ ⟨(1st β€˜π‘€), (2nd β€˜π‘§)⟩ ∈ π‘₯) β†’ βˆƒπ‘Ž ∈ βˆͺ π‘†βŸ¨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯)
7945, 75, 78syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ βˆƒπ‘Ž ∈ βˆͺ π‘†βŸ¨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯)
80 rabn0 4385 . . . . . . . . . . . . . . . . 17 ({π‘Ž ∈ βˆͺ 𝑆 ∣ ⟨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯} β‰  βˆ… ↔ βˆƒπ‘Ž ∈ βˆͺ π‘†βŸ¨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯)
8179, 80sylibr 233 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ {π‘Ž ∈ βˆͺ 𝑆 ∣ ⟨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯} β‰  βˆ…)
82 cnclima 22771 . . . . . . . . . . . . . . . . . 18 (((π‘Ž ∈ βˆͺ 𝑆 ↦ ⟨(1st β€˜π‘€), π‘ŽβŸ©) ∈ (𝑆 Cn (𝑅 Γ—t 𝑆)) ∧ π‘₯ ∈ (Clsdβ€˜(𝑅 Γ—t 𝑆))) β†’ (β—‘(π‘Ž ∈ βˆͺ 𝑆 ↦ ⟨(1st β€˜π‘€), π‘ŽβŸ©) β€œ π‘₯) ∈ (Clsdβ€˜π‘†))
8334, 65, 82syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (β—‘(π‘Ž ∈ βˆͺ 𝑆 ↦ ⟨(1st β€˜π‘€), π‘ŽβŸ©) β€œ π‘₯) ∈ (Clsdβ€˜π‘†))
8425, 83eqeltrrid 2838 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ {π‘Ž ∈ βˆͺ 𝑆 ∣ ⟨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯} ∈ (Clsdβ€˜π‘†))
8516, 13, 39, 81, 84connclo 22918 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ {π‘Ž ∈ βˆͺ 𝑆 ∣ ⟨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯} = βˆͺ 𝑆)
8623, 85eleqtrrd 2836 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ (2nd β€˜π‘€) ∈ {π‘Ž ∈ βˆͺ 𝑆 ∣ ⟨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯})
87 opeq2 4874 . . . . . . . . . . . . . . . . 17 (π‘Ž = (2nd β€˜π‘€) β†’ ⟨(1st β€˜π‘€), π‘ŽβŸ© = ⟨(1st β€˜π‘€), (2nd β€˜π‘€)⟩)
8887eleq1d 2818 . . . . . . . . . . . . . . . 16 (π‘Ž = (2nd β€˜π‘€) β†’ (⟨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯ ↔ ⟨(1st β€˜π‘€), (2nd β€˜π‘€)⟩ ∈ π‘₯))
8988elrab 3683 . . . . . . . . . . . . . . 15 ((2nd β€˜π‘€) ∈ {π‘Ž ∈ βˆͺ 𝑆 ∣ ⟨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯} ↔ ((2nd β€˜π‘€) ∈ βˆͺ 𝑆 ∧ ⟨(1st β€˜π‘€), (2nd β€˜π‘€)⟩ ∈ π‘₯))
9089simprbi 497 . . . . . . . . . . . . . 14 ((2nd β€˜π‘€) ∈ {π‘Ž ∈ βˆͺ 𝑆 ∣ ⟨(1st β€˜π‘€), π‘ŽβŸ© ∈ π‘₯} β†’ ⟨(1st β€˜π‘€), (2nd β€˜π‘€)⟩ ∈ π‘₯)
9186, 90syl 17 . . . . . . . . . . . . 13 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ ⟨(1st β€˜π‘€), (2nd β€˜π‘€)⟩ ∈ π‘₯)
9221, 91eqeltrd 2833 . . . . . . . . . . . 12 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ (𝑧 ∈ π‘₯ ∧ 𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆))) β†’ 𝑀 ∈ π‘₯)
9392expr 457 . . . . . . . . . . 11 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ 𝑧 ∈ π‘₯) β†’ (𝑀 ∈ βˆͺ (𝑅 Γ—t 𝑆) β†’ 𝑀 ∈ π‘₯))
9493ssrdv 3988 . . . . . . . . . 10 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ 𝑧 ∈ π‘₯) β†’ βˆͺ (𝑅 Γ—t 𝑆) βŠ† π‘₯)
959, 94eqssd 3999 . . . . . . . . 9 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) ∧ 𝑧 ∈ π‘₯) β†’ π‘₯ = βˆͺ (𝑅 Γ—t 𝑆))
9695ex 413 . . . . . . . 8 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) β†’ (𝑧 ∈ π‘₯ β†’ π‘₯ = βˆͺ (𝑅 Γ—t 𝑆)))
9796exlimdv 1936 . . . . . . 7 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) β†’ (βˆƒπ‘§ 𝑧 ∈ π‘₯ β†’ π‘₯ = βˆͺ (𝑅 Γ—t 𝑆)))
985, 97biimtrid 241 . . . . . 6 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) β†’ (Β¬ π‘₯ = βˆ… β†’ π‘₯ = βˆͺ (𝑅 Γ—t 𝑆)))
9998orrd 861 . . . . 5 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆)))) β†’ (π‘₯ = βˆ… ∨ π‘₯ = βˆͺ (𝑅 Γ—t 𝑆)))
10099ex 413 . . . 4 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) β†’ (π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆))) β†’ (π‘₯ = βˆ… ∨ π‘₯ = βˆͺ (𝑅 Γ—t 𝑆))))
101 vex 3478 . . . . 5 π‘₯ ∈ V
102101elpr 4651 . . . 4 (π‘₯ ∈ {βˆ…, βˆͺ (𝑅 Γ—t 𝑆)} ↔ (π‘₯ = βˆ… ∨ π‘₯ = βˆͺ (𝑅 Γ—t 𝑆)))
103100, 102syl6ibr 251 . . 3 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) β†’ (π‘₯ ∈ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆))) β†’ π‘₯ ∈ {βˆ…, βˆͺ (𝑅 Γ—t 𝑆)}))
104103ssrdv 3988 . 2 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) β†’ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆))) βŠ† {βˆ…, βˆͺ (𝑅 Γ—t 𝑆)})
105 eqid 2732 . . 3 βˆͺ (𝑅 Γ—t 𝑆) = βˆͺ (𝑅 Γ—t 𝑆)
106105isconn2 22917 . 2 ((𝑅 Γ—t 𝑆) ∈ Conn ↔ ((𝑅 Γ—t 𝑆) ∈ Top ∧ ((𝑅 Γ—t 𝑆) ∩ (Clsdβ€˜(𝑅 Γ—t 𝑆))) βŠ† {βˆ…, βˆͺ (𝑅 Γ—t 𝑆)}))
1074, 104, 106sylanbrc 583 1 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) β†’ (𝑅 Γ—t 𝑆) ∈ Conn)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 396   ∨ wo 845   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106   β‰  wne 2940  βˆƒwrex 3070  {crab 3432   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  {cpr 4630  βŸ¨cop 4634  βˆͺ cuni 4908   ↦ cmpt 5231   Γ— cxp 5674  β—‘ccnv 5675   β€œ cima 5679  β€˜cfv 6543  (class class class)co 7408  1st c1st 7972  2nd c2nd 7973  Topctop 22394  TopOnctopon 22411  Clsdccld 22519   Cn ccn 22727  Conncconn 22914   Γ—t ctx 23063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7411  df-oprab 7412  df-mpo 7413  df-1st 7974  df-2nd 7975  df-map 8821  df-topgen 17388  df-top 22395  df-topon 22412  df-bases 22448  df-cld 22522  df-cn 22730  df-cnp 22731  df-conn 22915  df-tx 23065
This theorem is referenced by:  cvmlift2lem9  34297  cvmlift2lem13  34301
  Copyright terms: Public domain W3C validator