This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem txconn

Description: The topological product of two connected spaces is connected. (Contributed by Mario Carneiro, 29-Mar-2015)

Ref Expression
Assertion txconn 
|- ( ( R e. Conn /\ S e. Conn ) -> ( R tX S ) e. Conn )

Proof

Step Hyp Ref Expression
1 conntop 
 |-  ( R e. Conn -> R e. Top )
2 conntop 
 |-  ( S e. Conn -> S e. Top )
3 txtop 
 |-  ( ( R e. Top /\ S e. Top ) -> ( R tX S ) e. Top )
4 1 2 3 syl2an 
 |-  ( ( R e. Conn /\ S e. Conn ) -> ( R tX S ) e. Top )
5 neq0 
 |-  ( -. x = (/) <-> E. z z e. x )
6 simplr 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ z e. x ) -> x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) )
7 6 elin1d 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ z e. x ) -> x e. ( R tX S ) )
8 elssuni 
 |-  ( x e. ( R tX S ) -> x C_ U. ( R tX S ) )
9 7 8 syl 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ z e. x ) -> x C_ U. ( R tX S ) )
10 simprr 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> w e. U. ( R tX S ) )
11 simplll 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> R e. Conn )
12 11 1 syl 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> R e. Top )
13 simpllr 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> S e. Conn )
14 13 2 syl 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> S e. Top )
15 eqid 
 |-  U. R = U. R
16 eqid 
 |-  U. S = U. S
17 15 16 txuni 
 |-  ( ( R e. Top /\ S e. Top ) -> ( U. R X. U. S ) = U. ( R tX S ) )
18 12 14 17 syl2anc 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> ( U. R X. U. S ) = U. ( R tX S ) )
19 10 18 eleqtrrd 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> w e. ( U. R X. U. S ) )
20 1st2nd2 
 |-  ( w e. ( U. R X. U. S ) -> w = <. ( 1st ` w ) , ( 2nd ` w ) >. )
21 19 20 syl 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> w = <. ( 1st ` w ) , ( 2nd ` w ) >. )
22 xp2nd 
 |-  ( w e. ( U. R X. U. S ) -> ( 2nd ` w ) e. U. S )
23 19 22 syl 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> ( 2nd ` w ) e. U. S )
24 eqid 
 |-  ( a e. U. S |-> <. ( 1st ` w ) , a >. ) = ( a e. U. S |-> <. ( 1st ` w ) , a >. )
25 24 mptpreima 
 |-  ( `' ( a e. U. S |-> <. ( 1st ` w ) , a >. ) " x ) = { a e. U. S | <. ( 1st ` w ) , a >. e. x }
26 toptopon2 
 |-  ( S e. Top <-> S e. ( TopOn ` U. S ) )
27 14 26 sylib 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> S e. ( TopOn ` U. S ) )
28 toptopon2 
 |-  ( R e. Top <-> R e. ( TopOn ` U. R ) )
29 12 28 sylib 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> R e. ( TopOn ` U. R ) )
30 xp1st 
 |-  ( w e. ( U. R X. U. S ) -> ( 1st ` w ) e. U. R )
31 19 30 syl 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> ( 1st ` w ) e. U. R )
32 27 29 31 cnmptc 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> ( a e. U. S |-> ( 1st ` w ) ) e. ( S Cn R ) )
33 27 cnmptid 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> ( a e. U. S |-> a ) e. ( S Cn S ) )
34 27 32 33 cnmpt1t 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> ( a e. U. S |-> <. ( 1st ` w ) , a >. ) e. ( S Cn ( R tX S ) ) )
35 simplr 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) )
36 35 elin1d 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> x e. ( R tX S ) )
37 cnima 
 |-  ( ( ( a e. U. S |-> <. ( 1st ` w ) , a >. ) e. ( S Cn ( R tX S ) ) /\ x e. ( R tX S ) ) -> ( `' ( a e. U. S |-> <. ( 1st ` w ) , a >. ) " x ) e. S )
38 34 36 37 syl2anc 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> ( `' ( a e. U. S |-> <. ( 1st ` w ) , a >. ) " x ) e. S )
39 25 38 eqeltrrid 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> { a e. U. S | <. ( 1st ` w ) , a >. e. x } e. S )
40 simprl 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> z e. x )
41 elunii 
 |-  ( ( z e. x /\ x e. ( R tX S ) ) -> z e. U. ( R tX S ) )
42 40 36 41 syl2anc 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> z e. U. ( R tX S ) )
43 42 18 eleqtrrd 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> z e. ( U. R X. U. S ) )
44 xp2nd 
 |-  ( z e. ( U. R X. U. S ) -> ( 2nd ` z ) e. U. S )
45 43 44 syl 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> ( 2nd ` z ) e. U. S )
46 eqid 
 |-  ( a e. U. R |-> <. a , ( 2nd ` z ) >. ) = ( a e. U. R |-> <. a , ( 2nd ` z ) >. )
47 46 mptpreima 
 |-  ( `' ( a e. U. R |-> <. a , ( 2nd ` z ) >. ) " x ) = { a e. U. R | <. a , ( 2nd ` z ) >. e. x }
48 29 cnmptid 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> ( a e. U. R |-> a ) e. ( R Cn R ) )
49 29 27 45 cnmptc 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> ( a e. U. R |-> ( 2nd ` z ) ) e. ( R Cn S ) )
50 29 48 49 cnmpt1t 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> ( a e. U. R |-> <. a , ( 2nd ` z ) >. ) e. ( R Cn ( R tX S ) ) )
51 cnima 
 |-  ( ( ( a e. U. R |-> <. a , ( 2nd ` z ) >. ) e. ( R Cn ( R tX S ) ) /\ x e. ( R tX S ) ) -> ( `' ( a e. U. R |-> <. a , ( 2nd ` z ) >. ) " x ) e. R )
52 50 36 51 syl2anc 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> ( `' ( a e. U. R |-> <. a , ( 2nd ` z ) >. ) " x ) e. R )
53 47 52 eqeltrrid 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> { a e. U. R | <. a , ( 2nd ` z ) >. e. x } e. R )
54 xp1st 
 |-  ( z e. ( U. R X. U. S ) -> ( 1st ` z ) e. U. R )
55 43 54 syl 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> ( 1st ` z ) e. U. R )
56 1st2nd2 
 |-  ( z e. ( U. R X. U. S ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
57 43 56 syl 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
58 57 40 eqeltrrd 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> <. ( 1st ` z ) , ( 2nd ` z ) >. e. x )
59 opeq1 
 |-  ( a = ( 1st ` z ) -> <. a , ( 2nd ` z ) >. = <. ( 1st ` z ) , ( 2nd ` z ) >. )
60 59 eleq1d 
 |-  ( a = ( 1st ` z ) -> ( <. a , ( 2nd ` z ) >. e. x <-> <. ( 1st ` z ) , ( 2nd ` z ) >. e. x ) )
61 60 rspcev 
 |-  ( ( ( 1st ` z ) e. U. R /\ <. ( 1st ` z ) , ( 2nd ` z ) >. e. x ) -> E. a e. U. R <. a , ( 2nd ` z ) >. e. x )
62 55 58 61 syl2anc 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> E. a e. U. R <. a , ( 2nd ` z ) >. e. x )
63 rabn0 
 |-  ( { a e. U. R | <. a , ( 2nd ` z ) >. e. x } =/= (/) <-> E. a e. U. R <. a , ( 2nd ` z ) >. e. x )
64 62 63 sylibr 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> { a e. U. R | <. a , ( 2nd ` z ) >. e. x } =/= (/) )
65 35 elin2d 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> x e. ( Clsd ` ( R tX S ) ) )
66 cnclima 
 |-  ( ( ( a e. U. R |-> <. a , ( 2nd ` z ) >. ) e. ( R Cn ( R tX S ) ) /\ x e. ( Clsd ` ( R tX S ) ) ) -> ( `' ( a e. U. R |-> <. a , ( 2nd ` z ) >. ) " x ) e. ( Clsd ` R ) )
67 50 65 66 syl2anc 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> ( `' ( a e. U. R |-> <. a , ( 2nd ` z ) >. ) " x ) e. ( Clsd ` R ) )
68 47 67 eqeltrrid 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> { a e. U. R | <. a , ( 2nd ` z ) >. e. x } e. ( Clsd ` R ) )
69 15 11 53 64 68 connclo 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> { a e. U. R | <. a , ( 2nd ` z ) >. e. x } = U. R )
70 31 69 eleqtrrd 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> ( 1st ` w ) e. { a e. U. R | <. a , ( 2nd ` z ) >. e. x } )
71 opeq1 
 |-  ( a = ( 1st ` w ) -> <. a , ( 2nd ` z ) >. = <. ( 1st ` w ) , ( 2nd ` z ) >. )
72 71 eleq1d 
 |-  ( a = ( 1st ` w ) -> ( <. a , ( 2nd ` z ) >. e. x <-> <. ( 1st ` w ) , ( 2nd ` z ) >. e. x ) )
73 72 elrab 
 |-  ( ( 1st ` w ) e. { a e. U. R | <. a , ( 2nd ` z ) >. e. x } <-> ( ( 1st ` w ) e. U. R /\ <. ( 1st ` w ) , ( 2nd ` z ) >. e. x ) )
74 73 simprbi 
 |-  ( ( 1st ` w ) e. { a e. U. R | <. a , ( 2nd ` z ) >. e. x } -> <. ( 1st ` w ) , ( 2nd ` z ) >. e. x )
75 70 74 syl 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> <. ( 1st ` w ) , ( 2nd ` z ) >. e. x )
76 opeq2 
 |-  ( a = ( 2nd ` z ) -> <. ( 1st ` w ) , a >. = <. ( 1st ` w ) , ( 2nd ` z ) >. )
77 76 eleq1d 
 |-  ( a = ( 2nd ` z ) -> ( <. ( 1st ` w ) , a >. e. x <-> <. ( 1st ` w ) , ( 2nd ` z ) >. e. x ) )
78 77 rspcev 
 |-  ( ( ( 2nd ` z ) e. U. S /\ <. ( 1st ` w ) , ( 2nd ` z ) >. e. x ) -> E. a e. U. S <. ( 1st ` w ) , a >. e. x )
79 45 75 78 syl2anc 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> E. a e. U. S <. ( 1st ` w ) , a >. e. x )
80 rabn0 
 |-  ( { a e. U. S | <. ( 1st ` w ) , a >. e. x } =/= (/) <-> E. a e. U. S <. ( 1st ` w ) , a >. e. x )
81 79 80 sylibr 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> { a e. U. S | <. ( 1st ` w ) , a >. e. x } =/= (/) )
82 cnclima 
 |-  ( ( ( a e. U. S |-> <. ( 1st ` w ) , a >. ) e. ( S Cn ( R tX S ) ) /\ x e. ( Clsd ` ( R tX S ) ) ) -> ( `' ( a e. U. S |-> <. ( 1st ` w ) , a >. ) " x ) e. ( Clsd ` S ) )
83 34 65 82 syl2anc 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> ( `' ( a e. U. S |-> <. ( 1st ` w ) , a >. ) " x ) e. ( Clsd ` S ) )
84 25 83 eqeltrrid 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> { a e. U. S | <. ( 1st ` w ) , a >. e. x } e. ( Clsd ` S ) )
85 16 13 39 81 84 connclo 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> { a e. U. S | <. ( 1st ` w ) , a >. e. x } = U. S )
86 23 85 eleqtrrd 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> ( 2nd ` w ) e. { a e. U. S | <. ( 1st ` w ) , a >. e. x } )
87 opeq2 
 |-  ( a = ( 2nd ` w ) -> <. ( 1st ` w ) , a >. = <. ( 1st ` w ) , ( 2nd ` w ) >. )
88 87 eleq1d 
 |-  ( a = ( 2nd ` w ) -> ( <. ( 1st ` w ) , a >. e. x <-> <. ( 1st ` w ) , ( 2nd ` w ) >. e. x ) )
89 88 elrab 
 |-  ( ( 2nd ` w ) e. { a e. U. S | <. ( 1st ` w ) , a >. e. x } <-> ( ( 2nd ` w ) e. U. S /\ <. ( 1st ` w ) , ( 2nd ` w ) >. e. x ) )
90 89 simprbi 
 |-  ( ( 2nd ` w ) e. { a e. U. S | <. ( 1st ` w ) , a >. e. x } -> <. ( 1st ` w ) , ( 2nd ` w ) >. e. x )
91 86 90 syl 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> <. ( 1st ` w ) , ( 2nd ` w ) >. e. x )
92 21 91 eqeltrd 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ ( z e. x /\ w e. U. ( R tX S ) ) ) -> w e. x )
93 92 expr 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ z e. x ) -> ( w e. U. ( R tX S ) -> w e. x ) )
94 93 ssrdv 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ z e. x ) -> U. ( R tX S ) C_ x )
95 9 94 eqssd 
 |-  ( ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) /\ z e. x ) -> x = U. ( R tX S ) )
96 95 ex 
 |-  ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) -> ( z e. x -> x = U. ( R tX S ) ) )
97 96 exlimdv 
 |-  ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) -> ( E. z z e. x -> x = U. ( R tX S ) ) )
98 5 97 biimtrid 
 |-  ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) -> ( -. x = (/) -> x = U. ( R tX S ) ) )
99 98 orrd 
 |-  ( ( ( R e. Conn /\ S e. Conn ) /\ x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) ) -> ( x = (/) \/ x = U. ( R tX S ) ) )
100 99 ex 
 |-  ( ( R e. Conn /\ S e. Conn ) -> ( x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) -> ( x = (/) \/ x = U. ( R tX S ) ) ) )
101 vex 
 |-  x e. _V
102 101 elpr 
 |-  ( x e. { (/) , U. ( R tX S ) } <-> ( x = (/) \/ x = U. ( R tX S ) ) )
103 100 102 imbitrrdi 
 |-  ( ( R e. Conn /\ S e. Conn ) -> ( x e. ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) -> x e. { (/) , U. ( R tX S ) } ) )
104 103 ssrdv 
 |-  ( ( R e. Conn /\ S e. Conn ) -> ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) C_ { (/) , U. ( R tX S ) } )
105 eqid 
 |-  U. ( R tX S ) = U. ( R tX S )
106 105 isconn2 
 |-  ( ( R tX S ) e. Conn <-> ( ( R tX S ) e. Top /\ ( ( R tX S ) i^i ( Clsd ` ( R tX S ) ) ) C_ { (/) , U. ( R tX S ) } ) )
107 4 104 106 sylanbrc 
 |-  ( ( R e. Conn /\ S e. Conn ) -> ( R tX S ) e. Conn )