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

Metamath Proof Explorer

Theorem hauspwpwf1

Description: Lemma for hauspwpwdom . Points in the closure of a set in a Hausdorff space are characterized by the open neighborhoods they extend into the generating set. (Contributed by Mario Carneiro, 28-Jul-2015)

Ref Expression
Hypotheses hauspwpwf1.x 
|- X = U. J
hauspwpwf1.f 
|- F = ( x e. ( ( cls ` J ) ` A ) |-> { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } )
Assertion hauspwpwf1 
|- ( ( J e. Haus /\ A C_ X ) -> F : ( ( cls ` J ) ` A ) -1-1-> ~P ~P A )

Proof

Step Hyp Ref Expression
1 hauspwpwf1.x 
 |-  X = U. J
2 hauspwpwf1.f 
 |-  F = ( x e. ( ( cls ` J ) ` A ) |-> { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } )
3 inss2 
 |-  ( j i^i A ) C_ A
4 vex 
 |-  j e. _V
5 4 inex1 
 |-  ( j i^i A ) e. _V
6 5 elpw 
 |-  ( ( j i^i A ) e. ~P A <-> ( j i^i A ) C_ A )
7 3 6 mpbir 
 |-  ( j i^i A ) e. ~P A
8 eleq1 
 |-  ( a = ( j i^i A ) -> ( a e. ~P A <-> ( j i^i A ) e. ~P A ) )
9 7 8 mpbiri 
 |-  ( a = ( j i^i A ) -> a e. ~P A )
10 9 adantl 
 |-  ( ( x e. j /\ a = ( j i^i A ) ) -> a e. ~P A )
11 10 rexlimivw 
 |-  ( E. j e. J ( x e. j /\ a = ( j i^i A ) ) -> a e. ~P A )
12 11 abssi 
 |-  { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } C_ ~P A
13 haustop 
 |-  ( J e. Haus -> J e. Top )
14 1 topopn 
 |-  ( J e. Top -> X e. J )
15 13 14 syl 
 |-  ( J e. Haus -> X e. J )
16 ssexg 
 |-  ( ( A C_ X /\ X e. J ) -> A e. _V )
17 15 16 sylan2 
 |-  ( ( A C_ X /\ J e. Haus ) -> A e. _V )
18 17 ancoms 
 |-  ( ( J e. Haus /\ A C_ X ) -> A e. _V )
19 pwexg 
 |-  ( A e. _V -> ~P A e. _V )
20 elpw2g 
 |-  ( ~P A e. _V -> ( { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } e. ~P ~P A <-> { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } C_ ~P A ) )
21 18 19 20 3syl 
 |-  ( ( J e. Haus /\ A C_ X ) -> ( { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } e. ~P ~P A <-> { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } C_ ~P A ) )
22 12 21 mpbiri 
 |-  ( ( J e. Haus /\ A C_ X ) -> { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } e. ~P ~P A )
23 22 a1d 
 |-  ( ( J e. Haus /\ A C_ X ) -> ( x e. ( ( cls ` J ) ` A ) -> { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } e. ~P ~P A ) )
24 simplll 
 |-  ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) -> J e. Haus )
25 1 clsss3 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( cls ` J ) ` A ) C_ X )
26 13 25 sylan 
 |-  ( ( J e. Haus /\ A C_ X ) -> ( ( cls ` J ) ` A ) C_ X )
27 26 ad2antrr 
 |-  ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) -> ( ( cls ` J ) ` A ) C_ X )
28 simplrl 
 |-  ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) -> x e. ( ( cls ` J ) ` A ) )
29 27 28 sseldd 
 |-  ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) -> x e. X )
30 simplrr 
 |-  ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) -> y e. ( ( cls ` J ) ` A ) )
31 27 30 sseldd 
 |-  ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) -> y e. X )
32 simpr 
 |-  ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) -> x =/= y )
33 1 hausnei 
 |-  ( ( J e. Haus /\ ( x e. X /\ y e. X /\ x =/= y ) ) -> E. k e. J E. l e. J ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) )
34 24 29 31 32 33 syl13anc 
 |-  ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) -> E. k e. J E. l e. J ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) )
35 simprll 
 |-  ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) -> k e. J )
36 simprr1 
 |-  ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) -> x e. k )
37 eqidd 
 |-  ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) -> ( k i^i A ) = ( k i^i A ) )
38 elequ2 
 |-  ( j = k -> ( x e. j <-> x e. k ) )
39 ineq1 
 |-  ( j = k -> ( j i^i A ) = ( k i^i A ) )
40 39 eqeq2d 
 |-  ( j = k -> ( ( k i^i A ) = ( j i^i A ) <-> ( k i^i A ) = ( k i^i A ) ) )
41 38 40 anbi12d 
 |-  ( j = k -> ( ( x e. j /\ ( k i^i A ) = ( j i^i A ) ) <-> ( x e. k /\ ( k i^i A ) = ( k i^i A ) ) ) )
42 41 rspcev 
 |-  ( ( k e. J /\ ( x e. k /\ ( k i^i A ) = ( k i^i A ) ) ) -> E. j e. J ( x e. j /\ ( k i^i A ) = ( j i^i A ) ) )
43 35 36 37 42 syl12anc 
 |-  ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) -> E. j e. J ( x e. j /\ ( k i^i A ) = ( j i^i A ) ) )
44 vex 
 |-  k e. _V
45 44 inex1 
 |-  ( k i^i A ) e. _V
46 eqeq1 
 |-  ( a = ( k i^i A ) -> ( a = ( j i^i A ) <-> ( k i^i A ) = ( j i^i A ) ) )
47 46 anbi2d 
 |-  ( a = ( k i^i A ) -> ( ( x e. j /\ a = ( j i^i A ) ) <-> ( x e. j /\ ( k i^i A ) = ( j i^i A ) ) ) )
48 47 rexbidv 
 |-  ( a = ( k i^i A ) -> ( E. j e. J ( x e. j /\ a = ( j i^i A ) ) <-> E. j e. J ( x e. j /\ ( k i^i A ) = ( j i^i A ) ) ) )
49 45 48 elab 
 |-  ( ( k i^i A ) e. { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } <-> E. j e. J ( x e. j /\ ( k i^i A ) = ( j i^i A ) ) )
50 43 49 sylibr 
 |-  ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) -> ( k i^i A ) e. { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } )
51 13 ad2antrr 
 |-  ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) -> J e. Top )
52 51 ad3antrrr 
 |-  ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ ( j e. J /\ y e. j ) ) -> J e. Top )
53 simplr 
 |-  ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) -> A C_ X )
54 53 ad3antrrr 
 |-  ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ ( j e. J /\ y e. j ) ) -> A C_ X )
55 simprr 
 |-  ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) -> y e. ( ( cls ` J ) ` A ) )
56 55 ad3antrrr 
 |-  ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ ( j e. J /\ y e. j ) ) -> y e. ( ( cls ` J ) ` A ) )
57 simplr 
 |-  ( ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) -> l e. J )
58 57 ad2antlr 
 |-  ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ ( j e. J /\ y e. j ) ) -> l e. J )
59 simprl 
 |-  ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ ( j e. J /\ y e. j ) ) -> j e. J )
60 inopn 
 |-  ( ( J e. Top /\ l e. J /\ j e. J ) -> ( l i^i j ) e. J )
61 52 58 59 60 syl3anc 
 |-  ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ ( j e. J /\ y e. j ) ) -> ( l i^i j ) e. J )
62 simpr2 
 |-  ( ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) -> y e. l )
63 62 ad2antlr 
 |-  ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ ( j e. J /\ y e. j ) ) -> y e. l )
64 simprr 
 |-  ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ ( j e. J /\ y e. j ) ) -> y e. j )
65 63 64 elind 
 |-  ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ ( j e. J /\ y e. j ) ) -> y e. ( l i^i j ) )
66 1 clsndisj 
 |-  ( ( ( J e. Top /\ A C_ X /\ y e. ( ( cls ` J ) ` A ) ) /\ ( ( l i^i j ) e. J /\ y e. ( l i^i j ) ) ) -> ( ( l i^i j ) i^i A ) =/= (/) )
67 52 54 56 61 65 66 syl32anc 
 |-  ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ ( j e. J /\ y e. j ) ) -> ( ( l i^i j ) i^i A ) =/= (/) )
68 n0 
 |-  ( ( ( l i^i j ) i^i A ) =/= (/) <-> E. z z e. ( ( l i^i j ) i^i A ) )
69 67 68 sylib 
 |-  ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ ( j e. J /\ y e. j ) ) -> E. z z e. ( ( l i^i j ) i^i A ) )
70 elin 
 |-  ( z e. ( ( l i^i j ) i^i A ) <-> ( z e. ( l i^i j ) /\ z e. A ) )
71 elin 
 |-  ( z e. ( l i^i j ) <-> ( z e. l /\ z e. j ) )
72 71 anbi1i 
 |-  ( ( z e. ( l i^i j ) /\ z e. A ) <-> ( ( z e. l /\ z e. j ) /\ z e. A ) )
73 70 72 bitri 
 |-  ( z e. ( ( l i^i j ) i^i A ) <-> ( ( z e. l /\ z e. j ) /\ z e. A ) )
74 elin 
 |-  ( z e. ( j i^i A ) <-> ( z e. j /\ z e. A ) )
75 74 biimpri 
 |-  ( ( z e. j /\ z e. A ) -> z e. ( j i^i A ) )
76 75 adantll 
 |-  ( ( ( z e. l /\ z e. j ) /\ z e. A ) -> z e. ( j i^i A ) )
77 76 ad2antll 
 |-  ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ ( ( j e. J /\ y e. j ) /\ ( ( z e. l /\ z e. j ) /\ z e. A ) ) ) -> z e. ( j i^i A ) )
78 simpll 
 |-  ( ( ( z e. l /\ z e. j ) /\ z e. A ) -> z e. l )
79 78 ad2antll 
 |-  ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ ( ( j e. J /\ y e. j ) /\ ( ( z e. l /\ z e. j ) /\ z e. A ) ) ) -> z e. l )
80 simpr3 
 |-  ( ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) -> ( k i^i l ) = (/) )
81 80 ad2antlr 
 |-  ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ ( ( j e. J /\ y e. j ) /\ ( ( z e. l /\ z e. j ) /\ z e. A ) ) ) -> ( k i^i l ) = (/) )
82 minel 
 |-  ( ( z e. l /\ ( k i^i l ) = (/) ) -> -. z e. k )
83 elinel1 
 |-  ( z e. ( k i^i A ) -> z e. k )
84 82 83 nsyl 
 |-  ( ( z e. l /\ ( k i^i l ) = (/) ) -> -. z e. ( k i^i A ) )
85 79 81 84 syl2anc 
 |-  ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ ( ( j e. J /\ y e. j ) /\ ( ( z e. l /\ z e. j ) /\ z e. A ) ) ) -> -. z e. ( k i^i A ) )
86 nelneq2 
 |-  ( ( z e. ( j i^i A ) /\ -. z e. ( k i^i A ) ) -> -. ( j i^i A ) = ( k i^i A ) )
87 77 85 86 syl2anc 
 |-  ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ ( ( j e. J /\ y e. j ) /\ ( ( z e. l /\ z e. j ) /\ z e. A ) ) ) -> -. ( j i^i A ) = ( k i^i A ) )
88 eqcom 
 |-  ( ( j i^i A ) = ( k i^i A ) <-> ( k i^i A ) = ( j i^i A ) )
89 87 88 sylnib 
 |-  ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ ( ( j e. J /\ y e. j ) /\ ( ( z e. l /\ z e. j ) /\ z e. A ) ) ) -> -. ( k i^i A ) = ( j i^i A ) )
90 89 expr 
 |-  ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ ( j e. J /\ y e. j ) ) -> ( ( ( z e. l /\ z e. j ) /\ z e. A ) -> -. ( k i^i A ) = ( j i^i A ) ) )
91 73 90 biimtrid 
 |-  ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ ( j e. J /\ y e. j ) ) -> ( z e. ( ( l i^i j ) i^i A ) -> -. ( k i^i A ) = ( j i^i A ) ) )
92 91 exlimdv 
 |-  ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ ( j e. J /\ y e. j ) ) -> ( E. z z e. ( ( l i^i j ) i^i A ) -> -. ( k i^i A ) = ( j i^i A ) ) )
93 69 92 mpd 
 |-  ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ ( j e. J /\ y e. j ) ) -> -. ( k i^i A ) = ( j i^i A ) )
94 93 anassrs 
 |-  ( ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ j e. J ) /\ y e. j ) -> -. ( k i^i A ) = ( j i^i A ) )
95 nan 
 |-  ( ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ j e. J ) -> -. ( y e. j /\ ( k i^i A ) = ( j i^i A ) ) ) <-> ( ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ j e. J ) /\ y e. j ) -> -. ( k i^i A ) = ( j i^i A ) ) )
96 94 95 mpbir 
 |-  ( ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) /\ j e. J ) -> -. ( y e. j /\ ( k i^i A ) = ( j i^i A ) ) )
97 96 nrexdv 
 |-  ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) -> -. E. j e. J ( y e. j /\ ( k i^i A ) = ( j i^i A ) ) )
98 46 anbi2d 
 |-  ( a = ( k i^i A ) -> ( ( y e. j /\ a = ( j i^i A ) ) <-> ( y e. j /\ ( k i^i A ) = ( j i^i A ) ) ) )
99 98 rexbidv 
 |-  ( a = ( k i^i A ) -> ( E. j e. J ( y e. j /\ a = ( j i^i A ) ) <-> E. j e. J ( y e. j /\ ( k i^i A ) = ( j i^i A ) ) ) )
100 45 99 elab 
 |-  ( ( k i^i A ) e. { a | E. j e. J ( y e. j /\ a = ( j i^i A ) ) } <-> E. j e. J ( y e. j /\ ( k i^i A ) = ( j i^i A ) ) )
101 97 100 sylnibr 
 |-  ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) -> -. ( k i^i A ) e. { a | E. j e. J ( y e. j /\ a = ( j i^i A ) ) } )
102 nelne1 
 |-  ( ( ( k i^i A ) e. { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } /\ -. ( k i^i A ) e. { a | E. j e. J ( y e. j /\ a = ( j i^i A ) ) } ) -> { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } =/= { a | E. j e. J ( y e. j /\ a = ( j i^i A ) ) } )
103 50 101 102 syl2anc 
 |-  ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( ( k e. J /\ l e. J ) /\ ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) ) ) -> { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } =/= { a | E. j e. J ( y e. j /\ a = ( j i^i A ) ) } )
104 103 expr 
 |-  ( ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) /\ ( k e. J /\ l e. J ) ) -> ( ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) -> { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } =/= { a | E. j e. J ( y e. j /\ a = ( j i^i A ) ) } ) )
105 104 rexlimdvva 
 |-  ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) -> ( E. k e. J E. l e. J ( x e. k /\ y e. l /\ ( k i^i l ) = (/) ) -> { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } =/= { a | E. j e. J ( y e. j /\ a = ( j i^i A ) ) } ) )
106 34 105 mpd 
 |-  ( ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) /\ x =/= y ) -> { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } =/= { a | E. j e. J ( y e. j /\ a = ( j i^i A ) ) } )
107 106 ex 
 |-  ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) -> ( x =/= y -> { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } =/= { a | E. j e. J ( y e. j /\ a = ( j i^i A ) ) } ) )
108 107 necon4d 
 |-  ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) -> ( { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } = { a | E. j e. J ( y e. j /\ a = ( j i^i A ) ) } -> x = y ) )
109 eleq1 
 |-  ( x = y -> ( x e. j <-> y e. j ) )
110 109 anbi1d 
 |-  ( x = y -> ( ( x e. j /\ a = ( j i^i A ) ) <-> ( y e. j /\ a = ( j i^i A ) ) ) )
111 110 rexbidv 
 |-  ( x = y -> ( E. j e. J ( x e. j /\ a = ( j i^i A ) ) <-> E. j e. J ( y e. j /\ a = ( j i^i A ) ) ) )
112 111 abbidv 
 |-  ( x = y -> { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } = { a | E. j e. J ( y e. j /\ a = ( j i^i A ) ) } )
113 108 112 impbid1 
 |-  ( ( ( J e. Haus /\ A C_ X ) /\ ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) ) -> ( { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } = { a | E. j e. J ( y e. j /\ a = ( j i^i A ) ) } <-> x = y ) )
114 113 ex 
 |-  ( ( J e. Haus /\ A C_ X ) -> ( ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( cls ` J ) ` A ) ) -> ( { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } = { a | E. j e. J ( y e. j /\ a = ( j i^i A ) ) } <-> x = y ) ) )
115 23 114 dom2lem 
 |-  ( ( J e. Haus /\ A C_ X ) -> ( x e. ( ( cls ` J ) ` A ) |-> { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } ) : ( ( cls ` J ) ` A ) -1-1-> ~P ~P A )
116 f1eq1 
 |-  ( F = ( x e. ( ( cls ` J ) ` A ) |-> { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } ) -> ( F : ( ( cls ` J ) ` A ) -1-1-> ~P ~P A <-> ( x e. ( ( cls ` J ) ` A ) |-> { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } ) : ( ( cls ` J ) ` A ) -1-1-> ~P ~P A ) )
117 2 116 ax-mp 
 |-  ( F : ( ( cls ` J ) ` A ) -1-1-> ~P ~P A <-> ( x e. ( ( cls ` J ) ` A ) |-> { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } ) : ( ( cls ` J ) ` A ) -1-1-> ~P ~P A )
118 115 117 sylibr 
 |-  ( ( J e. Haus /\ A C_ X ) -> F : ( ( cls ` J ) ` A ) -1-1-> ~P ~P A )