Metamath Proof Explorer

Theorem pthaus

Description: The product of a collection of Hausdorff spaces is Hausdorff. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion pthaus 
|- ( ( A e. V /\ F : A --> Haus ) -> ( Xt_ ` F ) e. Haus )

Proof

Step Hyp Ref Expression
1 haustop 
 |-  ( x e. Haus -> x e. Top )
2 1 ssriv 
 |-  Haus C_ Top
3 fss 
 |-  ( ( F : A --> Haus /\ Haus C_ Top ) -> F : A --> Top )
4 2 3 mpan2 
 |-  ( F : A --> Haus -> F : A --> Top )
5 pttop 
 |-  ( ( A e. V /\ F : A --> Top ) -> ( Xt_ ` F ) e. Top )
6 4 5 sylan2 
 |-  ( ( A e. V /\ F : A --> Haus ) -> ( Xt_ ` F ) e. Top )
7 simprl 
 |-  ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> x e. U. ( Xt_ ` F ) )
8 eqid 
 |-  ( Xt_ ` F ) = ( Xt_ ` F )
9 8 ptuni 
 |-  ( ( A e. V /\ F : A --> Top ) -> X_ k e. A U. ( F ` k ) = U. ( Xt_ ` F ) )
10 4 9 sylan2 
 |-  ( ( A e. V /\ F : A --> Haus ) -> X_ k e. A U. ( F ` k ) = U. ( Xt_ ` F ) )
11 10 adantr 
 |-  ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> X_ k e. A U. ( F ` k ) = U. ( Xt_ ` F ) )
12 7 11 eleqtrrd 
 |-  ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> x e. X_ k e. A U. ( F ` k ) )
13 ixpfn 
 |-  ( x e. X_ k e. A U. ( F ` k ) -> x Fn A )
14 12 13 syl 
 |-  ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> x Fn A )
15 simprr 
 |-  ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> y e. U. ( Xt_ ` F ) )
16 15 11 eleqtrrd 
 |-  ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> y e. X_ k e. A U. ( F ` k ) )
17 ixpfn 
 |-  ( y e. X_ k e. A U. ( F ` k ) -> y Fn A )
18 16 17 syl 
 |-  ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> y Fn A )
19 eqfnfv 
 |-  ( ( x Fn A /\ y Fn A ) -> ( x = y <-> A. k e. A ( x ` k ) = ( y ` k ) ) )
20 14 18 19 syl2anc 
 |-  ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> ( x = y <-> A. k e. A ( x ` k ) = ( y ` k ) ) )
21 20 necon3abid 
 |-  ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> ( x =/= y <-> -. A. k e. A ( x ` k ) = ( y ` k ) ) )
22 rexnal 
 |-  ( E. k e. A -. ( x ` k ) = ( y ` k ) <-> -. A. k e. A ( x ` k ) = ( y ` k ) )
23 df-ne 
 |-  ( ( x ` k ) =/= ( y ` k ) <-> -. ( x ` k ) = ( y ` k ) )
24 simpllr 
 |-  ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) -> F : A --> Haus )
25 simprl 
 |-  ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) -> k e. A )
26 24 25 ffvelcdmd 
 |-  ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) -> ( F ` k ) e. Haus )
27 vex 
 |-  x e. _V
28 27 elixp 
 |-  ( x e. X_ k e. A U. ( F ` k ) <-> ( x Fn A /\ A. k e. A ( x ` k ) e. U. ( F ` k ) ) )
29 28 simprbi 
 |-  ( x e. X_ k e. A U. ( F ` k ) -> A. k e. A ( x ` k ) e. U. ( F ` k ) )
30 12 29 syl 
 |-  ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> A. k e. A ( x ` k ) e. U. ( F ` k ) )
31 30 r19.21bi 
 |-  ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ k e. A ) -> ( x ` k ) e. U. ( F ` k ) )
32 31 adantrr 
 |-  ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) -> ( x ` k ) e. U. ( F ` k ) )
33 vex 
 |-  y e. _V
34 33 elixp 
 |-  ( y e. X_ k e. A U. ( F ` k ) <-> ( y Fn A /\ A. k e. A ( y ` k ) e. U. ( F ` k ) ) )
35 34 simprbi 
 |-  ( y e. X_ k e. A U. ( F ` k ) -> A. k e. A ( y ` k ) e. U. ( F ` k ) )
36 16 35 syl 
 |-  ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> A. k e. A ( y ` k ) e. U. ( F ` k ) )
37 36 r19.21bi 
 |-  ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ k e. A ) -> ( y ` k ) e. U. ( F ` k ) )
38 37 adantrr 
 |-  ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) -> ( y ` k ) e. U. ( F ` k ) )
39 simprr 
 |-  ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) -> ( x ` k ) =/= ( y ` k ) )
40 eqid 
 |-  U. ( F ` k ) = U. ( F ` k )
41 40 hausnei 
 |-  ( ( ( F ` k ) e. Haus /\ ( ( x ` k ) e. U. ( F ` k ) /\ ( y ` k ) e. U. ( F ` k ) /\ ( x ` k ) =/= ( y ` k ) ) ) -> E. m e. ( F ` k ) E. n e. ( F ` k ) ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) )
42 26 32 38 39 41 syl13anc 
 |-  ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) -> E. m e. ( F ` k ) E. n e. ( F ` k ) ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) )
43 simp-4l 
 |-  ( ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) /\ ( ( m e. ( F ` k ) /\ n e. ( F ` k ) ) /\ ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) ) ) -> A e. V )
44 4 ad4antlr 
 |-  ( ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) /\ ( ( m e. ( F ` k ) /\ n e. ( F ` k ) ) /\ ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) ) ) -> F : A --> Top )
45 25 adantr 
 |-  ( ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) /\ ( ( m e. ( F ` k ) /\ n e. ( F ` k ) ) /\ ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) ) ) -> k e. A )
46 eqid 
 |-  U. ( Xt_ ` F ) = U. ( Xt_ ` F )
47 46 8 ptpjcn 
 |-  ( ( A e. V /\ F : A --> Top /\ k e. A ) -> ( z e. U. ( Xt_ ` F ) |-> ( z ` k ) ) e. ( ( Xt_ ` F ) Cn ( F ` k ) ) )
48 43 44 45 47 syl3anc 
 |-  ( ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) /\ ( ( m e. ( F ` k ) /\ n e. ( F ` k ) ) /\ ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) ) ) -> ( z e. U. ( Xt_ ` F ) |-> ( z ` k ) ) e. ( ( Xt_ ` F ) Cn ( F ` k ) ) )
49 simprll 
 |-  ( ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) /\ ( ( m e. ( F ` k ) /\ n e. ( F ` k ) ) /\ ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) ) ) -> m e. ( F ` k ) )
50 eqid 
 |-  ( z e. U. ( Xt_ ` F ) |-> ( z ` k ) ) = ( z e. U. ( Xt_ ` F ) |-> ( z ` k ) )
51 50 mptpreima 
 |-  ( `' ( z e. U. ( Xt_ ` F ) |-> ( z ` k ) ) " m ) = { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m }
52 cnima 
 |-  ( ( ( z e. U. ( Xt_ ` F ) |-> ( z ` k ) ) e. ( ( Xt_ ` F ) Cn ( F ` k ) ) /\ m e. ( F ` k ) ) -> ( `' ( z e. U. ( Xt_ ` F ) |-> ( z ` k ) ) " m ) e. ( Xt_ ` F ) )
53 51 52 eqeltrrid 
 |-  ( ( ( z e. U. ( Xt_ ` F ) |-> ( z ` k ) ) e. ( ( Xt_ ` F ) Cn ( F ` k ) ) /\ m e. ( F ` k ) ) -> { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } e. ( Xt_ ` F ) )
54 48 49 53 syl2anc 
 |-  ( ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) /\ ( ( m e. ( F ` k ) /\ n e. ( F ` k ) ) /\ ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) ) ) -> { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } e. ( Xt_ ` F ) )
55 simprlr 
 |-  ( ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) /\ ( ( m e. ( F ` k ) /\ n e. ( F ` k ) ) /\ ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) ) ) -> n e. ( F ` k ) )
56 50 mptpreima 
 |-  ( `' ( z e. U. ( Xt_ ` F ) |-> ( z ` k ) ) " n ) = { z e. U. ( Xt_ ` F ) | ( z ` k ) e. n }
57 cnima 
 |-  ( ( ( z e. U. ( Xt_ ` F ) |-> ( z ` k ) ) e. ( ( Xt_ ` F ) Cn ( F ` k ) ) /\ n e. ( F ` k ) ) -> ( `' ( z e. U. ( Xt_ ` F ) |-> ( z ` k ) ) " n ) e. ( Xt_ ` F ) )
58 56 57 eqeltrrid 
 |-  ( ( ( z e. U. ( Xt_ ` F ) |-> ( z ` k ) ) e. ( ( Xt_ ` F ) Cn ( F ` k ) ) /\ n e. ( F ` k ) ) -> { z e. U. ( Xt_ ` F ) | ( z ` k ) e. n } e. ( Xt_ ` F ) )
59 48 55 58 syl2anc 
 |-  ( ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) /\ ( ( m e. ( F ` k ) /\ n e. ( F ` k ) ) /\ ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) ) ) -> { z e. U. ( Xt_ ` F ) | ( z ` k ) e. n } e. ( Xt_ ` F ) )
60 fveq1 
 |-  ( z = x -> ( z ` k ) = ( x ` k ) )
61 60 eleq1d 
 |-  ( z = x -> ( ( z ` k ) e. m <-> ( x ` k ) e. m ) )
62 7 ad2antrr 
 |-  ( ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) /\ ( ( m e. ( F ` k ) /\ n e. ( F ` k ) ) /\ ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) ) ) -> x e. U. ( Xt_ ` F ) )
63 simprr1 
 |-  ( ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) /\ ( ( m e. ( F ` k ) /\ n e. ( F ` k ) ) /\ ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) ) ) -> ( x ` k ) e. m )
64 61 62 63 elrabd 
 |-  ( ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) /\ ( ( m e. ( F ` k ) /\ n e. ( F ` k ) ) /\ ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) ) ) -> x e. { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } )
65 fveq1 
 |-  ( z = y -> ( z ` k ) = ( y ` k ) )
66 65 eleq1d 
 |-  ( z = y -> ( ( z ` k ) e. n <-> ( y ` k ) e. n ) )
67 15 ad2antrr 
 |-  ( ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) /\ ( ( m e. ( F ` k ) /\ n e. ( F ` k ) ) /\ ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) ) ) -> y e. U. ( Xt_ ` F ) )
68 simprr2 
 |-  ( ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) /\ ( ( m e. ( F ` k ) /\ n e. ( F ` k ) ) /\ ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) ) ) -> ( y ` k ) e. n )
69 66 67 68 elrabd 
 |-  ( ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) /\ ( ( m e. ( F ` k ) /\ n e. ( F ` k ) ) /\ ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) ) ) -> y e. { z e. U. ( Xt_ ` F ) | ( z ` k ) e. n } )
70 inrab 
 |-  ( { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } i^i { z e. U. ( Xt_ ` F ) | ( z ` k ) e. n } ) = { z e. U. ( Xt_ ` F ) | ( ( z ` k ) e. m /\ ( z ` k ) e. n ) }
71 simprr3 
 |-  ( ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) /\ ( ( m e. ( F ` k ) /\ n e. ( F ` k ) ) /\ ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) ) ) -> ( m i^i n ) = (/) )
72 inelcm 
 |-  ( ( ( z ` k ) e. m /\ ( z ` k ) e. n ) -> ( m i^i n ) =/= (/) )
73 72 necon2bi 
 |-  ( ( m i^i n ) = (/) -> -. ( ( z ` k ) e. m /\ ( z ` k ) e. n ) )
74 71 73 syl 
 |-  ( ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) /\ ( ( m e. ( F ` k ) /\ n e. ( F ` k ) ) /\ ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) ) ) -> -. ( ( z ` k ) e. m /\ ( z ` k ) e. n ) )
75 74 ralrimivw 
 |-  ( ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) /\ ( ( m e. ( F ` k ) /\ n e. ( F ` k ) ) /\ ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) ) ) -> A. z e. U. ( Xt_ ` F ) -. ( ( z ` k ) e. m /\ ( z ` k ) e. n ) )
76 rabeq0 
 |-  ( { z e. U. ( Xt_ ` F ) | ( ( z ` k ) e. m /\ ( z ` k ) e. n ) } = (/) <-> A. z e. U. ( Xt_ ` F ) -. ( ( z ` k ) e. m /\ ( z ` k ) e. n ) )
77 75 76 sylibr 
 |-  ( ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) /\ ( ( m e. ( F ` k ) /\ n e. ( F ` k ) ) /\ ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) ) ) -> { z e. U. ( Xt_ ` F ) | ( ( z ` k ) e. m /\ ( z ` k ) e. n ) } = (/) )
78 70 77 eqtrid 
 |-  ( ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) /\ ( ( m e. ( F ` k ) /\ n e. ( F ` k ) ) /\ ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) ) ) -> ( { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } i^i { z e. U. ( Xt_ ` F ) | ( z ` k ) e. n } ) = (/) )
79 eleq2 
 |-  ( u = { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } -> ( x e. u <-> x e. { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } ) )
80 ineq1 
 |-  ( u = { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } -> ( u i^i v ) = ( { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } i^i v ) )
81 80 eqeq1d 
 |-  ( u = { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } -> ( ( u i^i v ) = (/) <-> ( { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } i^i v ) = (/) ) )
82 79 81 3anbi13d 
 |-  ( u = { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } -> ( ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) <-> ( x e. { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } /\ y e. v /\ ( { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } i^i v ) = (/) ) ) )
83 eleq2 
 |-  ( v = { z e. U. ( Xt_ ` F ) | ( z ` k ) e. n } -> ( y e. v <-> y e. { z e. U. ( Xt_ ` F ) | ( z ` k ) e. n } ) )
84 ineq2 
 |-  ( v = { z e. U. ( Xt_ ` F ) | ( z ` k ) e. n } -> ( { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } i^i v ) = ( { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } i^i { z e. U. ( Xt_ ` F ) | ( z ` k ) e. n } ) )
85 84 eqeq1d 
 |-  ( v = { z e. U. ( Xt_ ` F ) | ( z ` k ) e. n } -> ( ( { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } i^i v ) = (/) <-> ( { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } i^i { z e. U. ( Xt_ ` F ) | ( z ` k ) e. n } ) = (/) ) )
86 83 85 3anbi23d 
 |-  ( v = { z e. U. ( Xt_ ` F ) | ( z ` k ) e. n } -> ( ( x e. { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } /\ y e. v /\ ( { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } i^i v ) = (/) ) <-> ( x e. { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } /\ y e. { z e. U. ( Xt_ ` F ) | ( z ` k ) e. n } /\ ( { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } i^i { z e. U. ( Xt_ ` F ) | ( z ` k ) e. n } ) = (/) ) ) )
87 82 86 rspc2ev 
 |-  ( ( { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } e. ( Xt_ ` F ) /\ { z e. U. ( Xt_ ` F ) | ( z ` k ) e. n } e. ( Xt_ ` F ) /\ ( x e. { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } /\ y e. { z e. U. ( Xt_ ` F ) | ( z ` k ) e. n } /\ ( { z e. U. ( Xt_ ` F ) | ( z ` k ) e. m } i^i { z e. U. ( Xt_ ` F ) | ( z ` k ) e. n } ) = (/) ) ) -> E. u e. ( Xt_ ` F ) E. v e. ( Xt_ ` F ) ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) )
88 54 59 64 69 78 87 syl113anc 
 |-  ( ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) /\ ( ( m e. ( F ` k ) /\ n e. ( F ` k ) ) /\ ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) ) ) -> E. u e. ( Xt_ ` F ) E. v e. ( Xt_ ` F ) ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) )
89 88 expr 
 |-  ( ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) /\ ( m e. ( F ` k ) /\ n e. ( F ` k ) ) ) -> ( ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) -> E. u e. ( Xt_ ` F ) E. v e. ( Xt_ ` F ) ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) ) )
90 89 rexlimdvva 
 |-  ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) -> ( E. m e. ( F ` k ) E. n e. ( F ` k ) ( ( x ` k ) e. m /\ ( y ` k ) e. n /\ ( m i^i n ) = (/) ) -> E. u e. ( Xt_ ` F ) E. v e. ( Xt_ ` F ) ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) ) )
91 42 90 mpd 
 |-  ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ ( k e. A /\ ( x ` k ) =/= ( y ` k ) ) ) -> E. u e. ( Xt_ ` F ) E. v e. ( Xt_ ` F ) ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) )
92 91 expr 
 |-  ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ k e. A ) -> ( ( x ` k ) =/= ( y ` k ) -> E. u e. ( Xt_ ` F ) E. v e. ( Xt_ ` F ) ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) ) )
93 23 92 biimtrrid 
 |-  ( ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) /\ k e. A ) -> ( -. ( x ` k ) = ( y ` k ) -> E. u e. ( Xt_ ` F ) E. v e. ( Xt_ ` F ) ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) ) )
94 93 rexlimdva 
 |-  ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> ( E. k e. A -. ( x ` k ) = ( y ` k ) -> E. u e. ( Xt_ ` F ) E. v e. ( Xt_ ` F ) ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) ) )
95 22 94 biimtrrid 
 |-  ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> ( -. A. k e. A ( x ` k ) = ( y ` k ) -> E. u e. ( Xt_ ` F ) E. v e. ( Xt_ ` F ) ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) ) )
96 21 95 sylbid 
 |-  ( ( ( A e. V /\ F : A --> Haus ) /\ ( x e. U. ( Xt_ ` F ) /\ y e. U. ( Xt_ ` F ) ) ) -> ( x =/= y -> E. u e. ( Xt_ ` F ) E. v e. ( Xt_ ` F ) ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) ) )
97 96 ralrimivva 
 |-  ( ( A e. V /\ F : A --> Haus ) -> A. x e. U. ( Xt_ ` F ) A. y e. U. ( Xt_ ` F ) ( x =/= y -> E. u e. ( Xt_ ` F ) E. v e. ( Xt_ ` F ) ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) ) )
98 46 ishaus 
 |-  ( ( Xt_ ` F ) e. Haus <-> ( ( Xt_ ` F ) e. Top /\ A. x e. U. ( Xt_ ` F ) A. y e. U. ( Xt_ ` F ) ( x =/= y -> E. u e. ( Xt_ ` F ) E. v e. ( Xt_ ` F ) ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) ) ) )
99 6 97 98 sylanbrc 
 |-  ( ( A e. V /\ F : A --> Haus ) -> ( Xt_ ` F ) e. Haus )