Metamath Proof Explorer

Theorem txhaus

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

Ref Expression
Assertion txhaus 
|- ( ( R e. Haus /\ S e. Haus ) -> ( R tX S ) e. Haus )

Proof

Step Hyp Ref Expression
1 haustop 
 |-  ( R e. Haus -> R e. Top )
2 haustop 
 |-  ( S e. Haus -> S e. Top )
3 txtop 
 |-  ( ( R e. Top /\ S e. Top ) -> ( R tX S ) e. Top )
4 1 2 3 syl2an 
 |-  ( ( R e. Haus /\ S e. Haus ) -> ( R tX S ) e. Top )
5 eqid 
 |-  U. R = U. R
6 eqid 
 |-  U. S = U. S
7 5 6 txuni 
 |-  ( ( R e. Top /\ S e. Top ) -> ( U. R X. U. S ) = U. ( R tX S ) )
8 1 2 7 syl2an 
 |-  ( ( R e. Haus /\ S e. Haus ) -> ( U. R X. U. S ) = U. ( R tX S ) )
9 8 eleq2d 
 |-  ( ( R e. Haus /\ S e. Haus ) -> ( x e. ( U. R X. U. S ) <-> x e. U. ( R tX S ) ) )
10 8 eleq2d 
 |-  ( ( R e. Haus /\ S e. Haus ) -> ( y e. ( U. R X. U. S ) <-> y e. U. ( R tX S ) ) )
11 9 10 anbi12d 
 |-  ( ( R e. Haus /\ S e. Haus ) -> ( ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) <-> ( x e. U. ( R tX S ) /\ y e. U. ( R tX S ) ) ) )
12 neorian 
 |-  ( ( ( 1st ` x ) =/= ( 1st ` y ) \/ ( 2nd ` x ) =/= ( 2nd ` y ) ) <-> -. ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) = ( 2nd ` y ) ) )
13 xpopth 
 |-  ( ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) -> ( ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) = ( 2nd ` y ) ) <-> x = y ) )
14 13 adantl 
 |-  ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) -> ( ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) = ( 2nd ` y ) ) <-> x = y ) )
15 14 necon3bbid 
 |-  ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) -> ( -. ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) = ( 2nd ` y ) ) <-> x =/= y ) )
16 12 15 bitrid 
 |-  ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) -> ( ( ( 1st ` x ) =/= ( 1st ` y ) \/ ( 2nd ` x ) =/= ( 2nd ` y ) ) <-> x =/= y ) )
17 simplll 
 |-  ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) -> R e. Haus )
18 xp1st 
 |-  ( x e. ( U. R X. U. S ) -> ( 1st ` x ) e. U. R )
19 18 ad2antrl 
 |-  ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) -> ( 1st ` x ) e. U. R )
20 19 adantr 
 |-  ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) -> ( 1st ` x ) e. U. R )
21 xp1st 
 |-  ( y e. ( U. R X. U. S ) -> ( 1st ` y ) e. U. R )
22 21 ad2antll 
 |-  ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) -> ( 1st ` y ) e. U. R )
23 22 adantr 
 |-  ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) -> ( 1st ` y ) e. U. R )
24 simpr 
 |-  ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) -> ( 1st ` x ) =/= ( 1st ` y ) )
25 5 hausnei 
 |-  ( ( R e. Haus /\ ( ( 1st ` x ) e. U. R /\ ( 1st ` y ) e. U. R /\ ( 1st ` x ) =/= ( 1st ` y ) ) ) -> E. u e. R E. v e. R ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) )
26 17 20 23 24 25 syl13anc 
 |-  ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) -> E. u e. R E. v e. R ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) )
27 1 ad2antrr 
 |-  ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) -> R e. Top )
28 27 ad2antrr 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) /\ ( ( u e. R /\ v e. R ) /\ ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> R e. Top )
29 2 ad4antlr 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) /\ ( ( u e. R /\ v e. R ) /\ ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> S e. Top )
30 simprll 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) /\ ( ( u e. R /\ v e. R ) /\ ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> u e. R )
31 6 topopn 
 |-  ( S e. Top -> U. S e. S )
32 29 31 syl 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) /\ ( ( u e. R /\ v e. R ) /\ ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> U. S e. S )
33 txopn 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( u e. R /\ U. S e. S ) ) -> ( u X. U. S ) e. ( R tX S ) )
34 28 29 30 32 33 syl22anc 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) /\ ( ( u e. R /\ v e. R ) /\ ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( u X. U. S ) e. ( R tX S ) )
35 simprlr 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) /\ ( ( u e. R /\ v e. R ) /\ ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> v e. R )
36 txopn 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( v e. R /\ U. S e. S ) ) -> ( v X. U. S ) e. ( R tX S ) )
37 28 29 35 32 36 syl22anc 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) /\ ( ( u e. R /\ v e. R ) /\ ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( v X. U. S ) e. ( R tX S ) )
38 1st2nd2 
 |-  ( x e. ( U. R X. U. S ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
39 38 ad2antrl 
 |-  ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
40 39 ad2antrr 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) /\ ( ( u e. R /\ v e. R ) /\ ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
41 simprr1 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) /\ ( ( u e. R /\ v e. R ) /\ ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( 1st ` x ) e. u )
42 xp2nd 
 |-  ( x e. ( U. R X. U. S ) -> ( 2nd ` x ) e. U. S )
43 42 ad2antrl 
 |-  ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) -> ( 2nd ` x ) e. U. S )
44 43 ad2antrr 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) /\ ( ( u e. R /\ v e. R ) /\ ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( 2nd ` x ) e. U. S )
45 41 44 jca 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) /\ ( ( u e. R /\ v e. R ) /\ ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( ( 1st ` x ) e. u /\ ( 2nd ` x ) e. U. S ) )
46 elxp6 
 |-  ( x e. ( u X. U. S ) <-> ( x = <. ( 1st ` x ) , ( 2nd ` x ) >. /\ ( ( 1st ` x ) e. u /\ ( 2nd ` x ) e. U. S ) ) )
47 40 45 46 sylanbrc 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) /\ ( ( u e. R /\ v e. R ) /\ ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> x e. ( u X. U. S ) )
48 1st2nd2 
 |-  ( y e. ( U. R X. U. S ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
49 48 ad2antll 
 |-  ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
50 49 ad2antrr 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) /\ ( ( u e. R /\ v e. R ) /\ ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
51 simprr2 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) /\ ( ( u e. R /\ v e. R ) /\ ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( 1st ` y ) e. v )
52 xp2nd 
 |-  ( y e. ( U. R X. U. S ) -> ( 2nd ` y ) e. U. S )
53 52 ad2antll 
 |-  ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) -> ( 2nd ` y ) e. U. S )
54 53 ad2antrr 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) /\ ( ( u e. R /\ v e. R ) /\ ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( 2nd ` y ) e. U. S )
55 51 54 jca 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) /\ ( ( u e. R /\ v e. R ) /\ ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( ( 1st ` y ) e. v /\ ( 2nd ` y ) e. U. S ) )
56 elxp6 
 |-  ( y e. ( v X. U. S ) <-> ( y = <. ( 1st ` y ) , ( 2nd ` y ) >. /\ ( ( 1st ` y ) e. v /\ ( 2nd ` y ) e. U. S ) ) )
57 50 55 56 sylanbrc 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) /\ ( ( u e. R /\ v e. R ) /\ ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> y e. ( v X. U. S ) )
58 simprr3 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) /\ ( ( u e. R /\ v e. R ) /\ ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( u i^i v ) = (/) )
59 58 xpeq1d 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) /\ ( ( u e. R /\ v e. R ) /\ ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( ( u i^i v ) X. U. S ) = ( (/) X. U. S ) )
60 xpindir 
 |-  ( ( u i^i v ) X. U. S ) = ( ( u X. U. S ) i^i ( v X. U. S ) )
61 0xp 
 |-  ( (/) X. U. S ) = (/)
62 59 60 61 3eqtr3g 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) /\ ( ( u e. R /\ v e. R ) /\ ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( ( u X. U. S ) i^i ( v X. U. S ) ) = (/) )
63 eleq2 
 |-  ( z = ( u X. U. S ) -> ( x e. z <-> x e. ( u X. U. S ) ) )
64 ineq1 
 |-  ( z = ( u X. U. S ) -> ( z i^i w ) = ( ( u X. U. S ) i^i w ) )
65 64 eqeq1d 
 |-  ( z = ( u X. U. S ) -> ( ( z i^i w ) = (/) <-> ( ( u X. U. S ) i^i w ) = (/) ) )
66 63 65 3anbi13d 
 |-  ( z = ( u X. U. S ) -> ( ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) <-> ( x e. ( u X. U. S ) /\ y e. w /\ ( ( u X. U. S ) i^i w ) = (/) ) ) )
67 eleq2 
 |-  ( w = ( v X. U. S ) -> ( y e. w <-> y e. ( v X. U. S ) ) )
68 ineq2 
 |-  ( w = ( v X. U. S ) -> ( ( u X. U. S ) i^i w ) = ( ( u X. U. S ) i^i ( v X. U. S ) ) )
69 68 eqeq1d 
 |-  ( w = ( v X. U. S ) -> ( ( ( u X. U. S ) i^i w ) = (/) <-> ( ( u X. U. S ) i^i ( v X. U. S ) ) = (/) ) )
70 67 69 3anbi23d 
 |-  ( w = ( v X. U. S ) -> ( ( x e. ( u X. U. S ) /\ y e. w /\ ( ( u X. U. S ) i^i w ) = (/) ) <-> ( x e. ( u X. U. S ) /\ y e. ( v X. U. S ) /\ ( ( u X. U. S ) i^i ( v X. U. S ) ) = (/) ) ) )
71 66 70 rspc2ev 
 |-  ( ( ( u X. U. S ) e. ( R tX S ) /\ ( v X. U. S ) e. ( R tX S ) /\ ( x e. ( u X. U. S ) /\ y e. ( v X. U. S ) /\ ( ( u X. U. S ) i^i ( v X. U. S ) ) = (/) ) ) -> E. z e. ( R tX S ) E. w e. ( R tX S ) ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) )
72 34 37 47 57 62 71 syl113anc 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) /\ ( ( u e. R /\ v e. R ) /\ ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> E. z e. ( R tX S ) E. w e. ( R tX S ) ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) )
73 72 expr 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) /\ ( u e. R /\ v e. R ) ) -> ( ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) -> E. z e. ( R tX S ) E. w e. ( R tX S ) ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) ) )
74 73 rexlimdvva 
 |-  ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) -> ( E. u e. R E. v e. R ( ( 1st ` x ) e. u /\ ( 1st ` y ) e. v /\ ( u i^i v ) = (/) ) -> E. z e. ( R tX S ) E. w e. ( R tX S ) ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) ) )
75 26 74 mpd 
 |-  ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) -> E. z e. ( R tX S ) E. w e. ( R tX S ) ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) )
76 simpllr 
 |-  ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) -> S e. Haus )
77 43 adantr 
 |-  ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) -> ( 2nd ` x ) e. U. S )
78 53 adantr 
 |-  ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) -> ( 2nd ` y ) e. U. S )
79 simpr 
 |-  ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) -> ( 2nd ` x ) =/= ( 2nd ` y ) )
80 6 hausnei 
 |-  ( ( S e. Haus /\ ( ( 2nd ` x ) e. U. S /\ ( 2nd ` y ) e. U. S /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) ) -> E. u e. S E. v e. S ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) )
81 76 77 78 79 80 syl13anc 
 |-  ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) -> E. u e. S E. v e. S ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) )
82 27 ad2antrr 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) /\ ( ( u e. S /\ v e. S ) /\ ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> R e. Top )
83 2 ad4antlr 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) /\ ( ( u e. S /\ v e. S ) /\ ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> S e. Top )
84 5 topopn 
 |-  ( R e. Top -> U. R e. R )
85 82 84 syl 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) /\ ( ( u e. S /\ v e. S ) /\ ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> U. R e. R )
86 simprll 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) /\ ( ( u e. S /\ v e. S ) /\ ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> u e. S )
87 txopn 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( U. R e. R /\ u e. S ) ) -> ( U. R X. u ) e. ( R tX S ) )
88 82 83 85 86 87 syl22anc 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) /\ ( ( u e. S /\ v e. S ) /\ ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( U. R X. u ) e. ( R tX S ) )
89 simprlr 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) /\ ( ( u e. S /\ v e. S ) /\ ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> v e. S )
90 txopn 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( U. R e. R /\ v e. S ) ) -> ( U. R X. v ) e. ( R tX S ) )
91 82 83 85 89 90 syl22anc 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) /\ ( ( u e. S /\ v e. S ) /\ ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( U. R X. v ) e. ( R tX S ) )
92 39 ad2antrr 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) /\ ( ( u e. S /\ v e. S ) /\ ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
93 19 ad2antrr 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) /\ ( ( u e. S /\ v e. S ) /\ ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( 1st ` x ) e. U. R )
94 simprr1 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) /\ ( ( u e. S /\ v e. S ) /\ ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( 2nd ` x ) e. u )
95 93 94 jca 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) /\ ( ( u e. S /\ v e. S ) /\ ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( ( 1st ` x ) e. U. R /\ ( 2nd ` x ) e. u ) )
96 elxp6 
 |-  ( x e. ( U. R X. u ) <-> ( x = <. ( 1st ` x ) , ( 2nd ` x ) >. /\ ( ( 1st ` x ) e. U. R /\ ( 2nd ` x ) e. u ) ) )
97 92 95 96 sylanbrc 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) /\ ( ( u e. S /\ v e. S ) /\ ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> x e. ( U. R X. u ) )
98 49 ad2antrr 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) /\ ( ( u e. S /\ v e. S ) /\ ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
99 22 ad2antrr 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) /\ ( ( u e. S /\ v e. S ) /\ ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( 1st ` y ) e. U. R )
100 simprr2 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) /\ ( ( u e. S /\ v e. S ) /\ ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( 2nd ` y ) e. v )
101 99 100 jca 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) /\ ( ( u e. S /\ v e. S ) /\ ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( ( 1st ` y ) e. U. R /\ ( 2nd ` y ) e. v ) )
102 elxp6 
 |-  ( y e. ( U. R X. v ) <-> ( y = <. ( 1st ` y ) , ( 2nd ` y ) >. /\ ( ( 1st ` y ) e. U. R /\ ( 2nd ` y ) e. v ) ) )
103 98 101 102 sylanbrc 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) /\ ( ( u e. S /\ v e. S ) /\ ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> y e. ( U. R X. v ) )
104 simprr3 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) /\ ( ( u e. S /\ v e. S ) /\ ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( u i^i v ) = (/) )
105 104 xpeq2d 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) /\ ( ( u e. S /\ v e. S ) /\ ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( U. R X. ( u i^i v ) ) = ( U. R X. (/) ) )
106 xpindi 
 |-  ( U. R X. ( u i^i v ) ) = ( ( U. R X. u ) i^i ( U. R X. v ) )
107 xp0 
 |-  ( U. R X. (/) ) = (/)
108 105 106 107 3eqtr3g 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) /\ ( ( u e. S /\ v e. S ) /\ ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( ( U. R X. u ) i^i ( U. R X. v ) ) = (/) )
109 eleq2 
 |-  ( z = ( U. R X. u ) -> ( x e. z <-> x e. ( U. R X. u ) ) )
110 ineq1 
 |-  ( z = ( U. R X. u ) -> ( z i^i w ) = ( ( U. R X. u ) i^i w ) )
111 110 eqeq1d 
 |-  ( z = ( U. R X. u ) -> ( ( z i^i w ) = (/) <-> ( ( U. R X. u ) i^i w ) = (/) ) )
112 109 111 3anbi13d 
 |-  ( z = ( U. R X. u ) -> ( ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) <-> ( x e. ( U. R X. u ) /\ y e. w /\ ( ( U. R X. u ) i^i w ) = (/) ) ) )
113 eleq2 
 |-  ( w = ( U. R X. v ) -> ( y e. w <-> y e. ( U. R X. v ) ) )
114 ineq2 
 |-  ( w = ( U. R X. v ) -> ( ( U. R X. u ) i^i w ) = ( ( U. R X. u ) i^i ( U. R X. v ) ) )
115 114 eqeq1d 
 |-  ( w = ( U. R X. v ) -> ( ( ( U. R X. u ) i^i w ) = (/) <-> ( ( U. R X. u ) i^i ( U. R X. v ) ) = (/) ) )
116 113 115 3anbi23d 
 |-  ( w = ( U. R X. v ) -> ( ( x e. ( U. R X. u ) /\ y e. w /\ ( ( U. R X. u ) i^i w ) = (/) ) <-> ( x e. ( U. R X. u ) /\ y e. ( U. R X. v ) /\ ( ( U. R X. u ) i^i ( U. R X. v ) ) = (/) ) ) )
117 112 116 rspc2ev 
 |-  ( ( ( U. R X. u ) e. ( R tX S ) /\ ( U. R X. v ) e. ( R tX S ) /\ ( x e. ( U. R X. u ) /\ y e. ( U. R X. v ) /\ ( ( U. R X. u ) i^i ( U. R X. v ) ) = (/) ) ) -> E. z e. ( R tX S ) E. w e. ( R tX S ) ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) )
118 88 91 97 103 108 117 syl113anc 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) /\ ( ( u e. S /\ v e. S ) /\ ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> E. z e. ( R tX S ) E. w e. ( R tX S ) ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) )
119 118 expr 
 |-  ( ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) /\ ( u e. S /\ v e. S ) ) -> ( ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) -> E. z e. ( R tX S ) E. w e. ( R tX S ) ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) ) )
120 119 rexlimdvva 
 |-  ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) -> ( E. u e. S E. v e. S ( ( 2nd ` x ) e. u /\ ( 2nd ` y ) e. v /\ ( u i^i v ) = (/) ) -> E. z e. ( R tX S ) E. w e. ( R tX S ) ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) ) )
121 81 120 mpd 
 |-  ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( 2nd ` x ) =/= ( 2nd ` y ) ) -> E. z e. ( R tX S ) E. w e. ( R tX S ) ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) )
122 75 121 jaodan 
 |-  ( ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) /\ ( ( 1st ` x ) =/= ( 1st ` y ) \/ ( 2nd ` x ) =/= ( 2nd ` y ) ) ) -> E. z e. ( R tX S ) E. w e. ( R tX S ) ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) )
123 122 ex 
 |-  ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) -> ( ( ( 1st ` x ) =/= ( 1st ` y ) \/ ( 2nd ` x ) =/= ( 2nd ` y ) ) -> E. z e. ( R tX S ) E. w e. ( R tX S ) ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) ) )
124 16 123 sylbird 
 |-  ( ( ( R e. Haus /\ S e. Haus ) /\ ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) ) -> ( x =/= y -> E. z e. ( R tX S ) E. w e. ( R tX S ) ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) ) )
125 124 ex 
 |-  ( ( R e. Haus /\ S e. Haus ) -> ( ( x e. ( U. R X. U. S ) /\ y e. ( U. R X. U. S ) ) -> ( x =/= y -> E. z e. ( R tX S ) E. w e. ( R tX S ) ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) ) ) )
126 11 125 sylbird 
 |-  ( ( R e. Haus /\ S e. Haus ) -> ( ( x e. U. ( R tX S ) /\ y e. U. ( R tX S ) ) -> ( x =/= y -> E. z e. ( R tX S ) E. w e. ( R tX S ) ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) ) ) )
127 126 ralrimivv 
 |-  ( ( R e. Haus /\ S e. Haus ) -> A. x e. U. ( R tX S ) A. y e. U. ( R tX S ) ( x =/= y -> E. z e. ( R tX S ) E. w e. ( R tX S ) ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) ) )
128 eqid 
 |-  U. ( R tX S ) = U. ( R tX S )
129 128 ishaus 
 |-  ( ( R tX S ) e. Haus <-> ( ( R tX S ) e. Top /\ A. x e. U. ( R tX S ) A. y e. U. ( R tX S ) ( x =/= y -> E. z e. ( R tX S ) E. w e. ( R tX S ) ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) ) ) )
130 4 127 129 sylanbrc 
 |-  ( ( R e. Haus /\ S e. Haus ) -> ( R tX S ) e. Haus )