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
|
syl5bi |
|- ( ( ( 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
|
syl6ibr |
|- ( ( 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 ) |