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 )