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 )