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 = ⋃ J$
	Assertion	hauspwpwdom	$⊢ (J \in Haus \land A \subseteq X) \to cls (J) (A) ≼ 𝒫 𝒫 A$

Proof

Step	Hyp	Ref	Expression
1		hauspwpwf1.x	$⊢ X = ⋃ J$
2		fvexd	$⊢ (J \in Haus \land A \subseteq X) \to cls (J) (A) \in V$
3		haustop	$⊢ J \in Haus \to J \in Top$
4	1	topopn	$⊢ J \in Top \to X \in J$
5	3 4	syl	$⊢ J \in Haus \to X \in J$
6	5	adantr	$⊢ (J \in Haus \land A \subseteq X) \to X \in J$
7		simpr	$⊢ (J \in Haus \land A \subseteq X) \to A \subseteq X$
8	6 7	ssexd	$⊢ (J \in Haus \land A \subseteq X) \to A \in V$
9		pwexg	$⊢ A \in V \to 𝒫 A \in V$
10		pwexg	$⊢ 𝒫 A \in V \to 𝒫 𝒫 A \in V$
11	8 9 10	3syl	$⊢ (J \in Haus \land A \subseteq X) \to 𝒫 𝒫 A \in V$
12		eqid	$⊢ (x \in cls (J) (A) ⟼ \{z \| \exists y \in J (x \in y \land z = y \cap A)\}) = (x \in cls (J) (A) ⟼ \{z \| \exists y \in J (x \in y \land z = y \cap A)\})$
13	1 12	hauspwpwf1	$⊢ (J \in Haus \land A \subseteq X) \to (x \in cls (J) (A) ⟼ \{z \| \exists y \in J (x \in y \land z = y \cap A)\}) : cls (J) (A) \underset{1-1}{⟶} 𝒫 𝒫 A$
14		f1dom2g	$⊢ (cls (J) (A) \in V \land 𝒫 𝒫 A \in V \land (x \in cls (J) (A) ⟼ \{z \| \exists y \in J (x \in y \land z = y \cap A)\}) : cls (J) (A) \underset{1-1}{⟶} 𝒫 𝒫 A) \to cls (J) (A) ≼ 𝒫 𝒫 A$
15	2 11 13 14	syl3anc	$⊢ (J \in Haus \land A \subseteq X) \to cls (J) (A) ≼ 𝒫 𝒫 A$

Metamath Proof Explorer

Theorem hauspwpwdom

Proof