dis1stc

Description: A discrete space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015)

		Ref	Expression
	Assertion	dis1stc	$⊢ X \in V \to 𝒫 X \in 1^{st} 𝜔$

Step	Hyp	Ref	Expression
1		vsnex	$⊢ \{x\} \in V$
2		distop	$⊢ \{x\} \in V \to 𝒫 \{x\} \in Top$
3	1 2	ax-mp	$⊢ 𝒫 \{x\} \in Top$
4		tgtop	$⊢ 𝒫 \{x\} \in Top \to topGen (𝒫 \{x\}) = 𝒫 \{x\}$
5	3 4	ax-mp	$⊢ topGen (𝒫 \{x\}) = 𝒫 \{x\}$
6		topbas	$⊢ 𝒫 \{x\} \in Top \to 𝒫 \{x\} \in TopBases$
7	3 6	ax-mp	$⊢ 𝒫 \{x\} \in TopBases$
8		snfi	$⊢ \{x\} \in Fin$
9		pwfi	$⊢ \{x\} \in Fin \leftrightarrow 𝒫 \{x\} \in Fin$
10	8 9	mpbi	$⊢ 𝒫 \{x\} \in Fin$
11		isfinite	$⊢ 𝒫 \{x\} \in Fin \leftrightarrow 𝒫 \{x\} ≺ ω$
12	10 11	mpbi	$⊢ 𝒫 \{x\} ≺ ω$
13		sdomdom	$⊢ 𝒫 \{x\} ≺ ω \to 𝒫 \{x\} ≼ ω$
14	12 13	ax-mp	$⊢ 𝒫 \{x\} ≼ ω$
15		2ndci	$⊢ (𝒫 \{x\} \in TopBases \land 𝒫 \{x\} ≼ ω) \to topGen (𝒫 \{x\}) \in 2^{nd} 𝜔$
16	7 14 15	mp2an	$⊢ topGen (𝒫 \{x\}) \in 2^{nd} 𝜔$
17	5 16	eqeltrri	$⊢ 𝒫 \{x\} \in 2^{nd} 𝜔$
18		2ndc1stc	$⊢ 𝒫 \{x\} \in 2^{nd} 𝜔 \to 𝒫 \{x\} \in 1^{st} 𝜔$
19	17 18	ax-mp	$⊢ 𝒫 \{x\} \in 1^{st} 𝜔$
20	19	rgenw	$⊢ \forall x \in X 𝒫 \{x\} \in 1^{st} 𝜔$
21		dislly	$⊢ X \in V \to (𝒫 X \in Locally1^{st} 𝜔\leftrightarrow\forall x \in X)$
22	20 21	mpbiri	$⊢ X \in V \to 𝒫 X \in Locally1^{st} 𝜔$
23		lly1stc	$⊢ Locally1^{st} 𝜔=1^{st} 𝜔$
24	22 23	eleqtrdi	$⊢ X \in V \to 𝒫 X \in 1^{st} 𝜔$

Metamath Proof Explorer