Step |
Hyp |
Ref |
Expression |
1 |
|
hauspwpwf1.x |
|- X = U. J |
2 |
|
fvexd |
|- ( ( J e. Haus /\ A C_ X ) -> ( ( cls ` J ) ` A ) e. _V ) |
3 |
|
haustop |
|- ( J e. Haus -> J e. Top ) |
4 |
1
|
topopn |
|- ( J e. Top -> X e. J ) |
5 |
3 4
|
syl |
|- ( J e. Haus -> X e. J ) |
6 |
5
|
adantr |
|- ( ( J e. Haus /\ A C_ X ) -> X e. J ) |
7 |
|
simpr |
|- ( ( J e. Haus /\ A C_ X ) -> A C_ X ) |
8 |
6 7
|
ssexd |
|- ( ( J e. Haus /\ A C_ X ) -> A e. _V ) |
9 |
|
pwexg |
|- ( A e. _V -> ~P A e. _V ) |
10 |
|
pwexg |
|- ( ~P A e. _V -> ~P ~P A e. _V ) |
11 |
8 9 10
|
3syl |
|- ( ( J e. Haus /\ A C_ X ) -> ~P ~P A e. _V ) |
12 |
|
eqid |
|- ( x e. ( ( cls ` J ) ` A ) |-> { z | E. y e. J ( x e. y /\ z = ( y i^i A ) ) } ) = ( x e. ( ( cls ` J ) ` A ) |-> { z | E. y e. J ( x e. y /\ z = ( y i^i A ) ) } ) |
13 |
1 12
|
hauspwpwf1 |
|- ( ( J e. Haus /\ A C_ X ) -> ( x e. ( ( cls ` J ) ` A ) |-> { z | E. y e. J ( x e. y /\ z = ( y i^i A ) ) } ) : ( ( cls ` J ) ` A ) -1-1-> ~P ~P A ) |
14 |
|
f1dom2g |
|- ( ( ( ( cls ` J ) ` A ) e. _V /\ ~P ~P A e. _V /\ ( x e. ( ( cls ` J ) ` A ) |-> { z | E. y e. J ( x e. y /\ z = ( y i^i A ) ) } ) : ( ( cls ` J ) ` A ) -1-1-> ~P ~P A ) -> ( ( cls ` J ) ` A ) ~<_ ~P ~P A ) |
15 |
2 11 13 14
|
syl3anc |
|- ( ( J e. Haus /\ A C_ X ) -> ( ( cls ` J ) ` A ) ~<_ ~P ~P A ) |