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 ⊢ 𝑋 = ∪ 𝐽
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 ‘ 𝐽 ) ‘ 𝐴 ) ≼ 𝒫 𝒫 𝐴 )