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

Metamath Proof Explorer

Theorem hauspwpwdom

Description: If X is a Hausdorff space, then the cardinality of the closure of a set A is bounded by the double powerset of A . In particular, a Hausdorff space with a dense subset A has cardinality at most ~P ~P A , and a separable Hausdorff space has cardinality at most ~P ~P NN . (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Mario Carneiro, 28-Jul-2015)

Ref Expression
Hypothesis hauspwpwf1.x 
|- X = U. J
Assertion hauspwpwdom 
|- ( ( J e. Haus /\ A C_ X ) -> ( ( cls ` J ) ` A ) ~<_ ~P ~P A )

Proof

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 )