hausmapdom

Description: If X is a first-countable Hausdorff space, then the cardinality of the closure of a set A is bounded by NN to the power A . In particular, a first-countable Hausdorff space with a dense subset A has cardinality at most A ^ NN , and a separable first-countable Hausdorff space has cardinality at most ~P NN . (Compare hauspwpwdom to see a weaker result if the assumption of first-countability is omitted.) (Contributed by Mario Carneiro, 9-Apr-2015)

		Ref	Expression
	Hypothesis	hauspwdom.1	$⊢ X = ⋃ J$
	Assertion	hausmapdom	$⊢ (J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \to cls (J) (A) ≼ (A^{ℕ})$

Proof

Step	Hyp	Ref	Expression
1		hauspwdom.1	$⊢ X = ⋃ J$
2	1	1stcelcls	$⊢ (J \in 1^{st} 𝜔 \land A \subseteq X) \to (x \in cls (J) (A) \leftrightarrow \exists f (f : ℕ ⟶ A \land f \underset{t}{⇝} (J) x))$
3	2	3adant1	$⊢ (J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \to (x \in cls (J) (A) \leftrightarrow \exists f (f : ℕ ⟶ A \land f \underset{t}{⇝} (J) x))$
4		uniexg	$⊢ J \in Haus \to ⋃ J \in V$
5	4	3ad2ant1	$⊢ (J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \to ⋃ J \in V$
6	1 5	eqeltrid	$⊢ (J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \to X \in V$
7		simp3	$⊢ (J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \to A \subseteq X$
8	6 7	ssexd	$⊢ (J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \to A \in V$
9		nnex	$⊢ ℕ \in V$
10		elmapg	$⊢ (A \in V \land ℕ \in V) \to (f \in (A^{ℕ}) \leftrightarrow f : ℕ ⟶ A)$
11	8 9 10	sylancl	$⊢ (J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \to (f \in (A^{ℕ}) \leftrightarrow f : ℕ ⟶ A)$
12	11	anbi1d	$⊢ (J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \to ((f \in (A^{ℕ}) \land f \underset{t}{⇝} (J) x) \leftrightarrow (f : ℕ ⟶ A \land f \underset{t}{⇝} (J) x))$
13	12	exbidv	$⊢ (J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \to (\exists f (f \in (A^{ℕ}) \land f \underset{t}{⇝} (J) x) \leftrightarrow \exists f (f : ℕ ⟶ A \land f \underset{t}{⇝} (J) x))$
14	3 13	bitr4d	$⊢ (J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \to (x \in cls (J) (A) \leftrightarrow \exists f (f \in (A^{ℕ}) \land f \underset{t}{⇝} (J) x))$
15		df-rex	$⊢ \exists f \in (A^{ℕ}) f \underset{t}{⇝} (J) x \leftrightarrow \exists f (f \in (A^{ℕ}) \land f \underset{t}{⇝} (J) x)$
16	14 15	bitr4di	$⊢ (J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \to (x \in cls (J) (A) \leftrightarrow \exists f \in (A^{ℕ}) f \underset{t}{⇝} (J) x)$
17		vex	$⊢ x \in V$
18	17	elima	$⊢ x \in \underset{t}{⇝} (J) [A^{ℕ}] \leftrightarrow \exists f \in (A^{ℕ}) f \underset{t}{⇝} (J) x$
19	16 18	bitr4di	$⊢ (J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \to (x \in cls (J) (A) \leftrightarrow x \in \underset{t}{⇝} (J) [A^{ℕ}])$
20	19	eqrdv	$⊢ (J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \to cls (J) (A) = \underset{t}{⇝} (J) [A^{ℕ}]$
21		ovex	$⊢ A^{ℕ} \in V$
22		lmfun	$⊢ J \in Haus \to Fun \underset{t}{⇝} (J)$
23	22	3ad2ant1	$⊢ (J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \to Fun \underset{t}{⇝} (J)$
24		imadomg	$⊢ A^{ℕ} \in V \to (Fun \underset{t}{⇝} (J) \to \underset{t}{⇝} (J) [A^{ℕ}] ≼ (A^{ℕ}))$
25	21 23 24	mpsyl	$⊢ (J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \to \underset{t}{⇝} (J) [A^{ℕ}] ≼ (A^{ℕ})$
26	20 25	eqbrtrd	$⊢ (J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \to cls (J) (A) ≼ (A^{ℕ})$

Metamath Proof Explorer

Theorem hausmapdom

Proof