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