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	⊢ 𝑋 = ∪ 𝐽
Assertion	hauspwpwdom	⊢ ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ≼ 𝒫 𝒫 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		hauspwpwf1.x	⊢ 𝑋 = ∪ 𝐽
2		fvexd	⊢ ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∈ V )
3		haustop	⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Top )
4	1	topopn	⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
5	3 4	syl	⊢ ( 𝐽 ∈ Haus → 𝑋 ∈ 𝐽 )
6	5	adantr	⊢ ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) → 𝑋 ∈ 𝐽 )
7		simpr	⊢ ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ⊆ 𝑋 )
8	6 7	ssexd	⊢ ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ∈ V )
9		pwexg	⊢ ( 𝐴 ∈ V → 𝒫 𝐴 ∈ V )
10		pwexg	⊢ ( 𝒫 𝐴 ∈ V → 𝒫 𝒫 𝐴 ∈ V )
11	8 9 10	3syl	⊢ ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) → 𝒫 𝒫 𝐴 ∈ V )
12		eqid	⊢ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↦ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝑧 = ( 𝑦 ∩ 𝐴 ) ) } ) = ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↦ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝑧 = ( 𝑦 ∩ 𝐴 ) ) } )
13	1 12	hauspwpwf1	⊢ ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↦ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝑧 = ( 𝑦 ∩ 𝐴 ) ) } ) : ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) –1-1→ 𝒫 𝒫 𝐴 )
14		f1dom2g	⊢ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∈ V ∧ 𝒫 𝒫 𝐴 ∈ V ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↦ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝑧 = ( 𝑦 ∩ 𝐴 ) ) } ) : ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) –1-1→ 𝒫 𝒫 𝐴 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ≼ 𝒫 𝒫 𝐴 )
15	2 11 13 14	syl3anc	⊢ ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ≼ 𝒫 𝒫 𝐴 )