dis2ndc

Description: A discrete space is second-countable iff it is countable. (Contributed by Mario Carneiro, 13-Apr-2015)

		Ref	Expression
	Assertion	dis2ndc	$⊢ X ≼ ω \leftrightarrow 𝒫 X \in 2^{nd} 𝜔$

Proof

Step	Hyp	Ref	Expression
1		ctex	$⊢ X ≼ ω \to X \in V$
2		pwexr	$⊢ 𝒫 X \in 2^{nd} 𝜔 \to X \in V$
3		vsnex	$⊢ \{x\} \in V$
4	3	2a1i	$⊢ X \in V \to (x \in X \to \{x\} \in V)$
5		vex	$⊢ x \in V$
6	5	sneqr	$⊢ \{x\} = \{y\} \to x = y$
7		sneq	$⊢ x = y \to \{x\} = \{y\}$
8	6 7	impbii	$⊢ \{x\} = \{y\} \leftrightarrow x = y$
9	8	2a1i	$⊢ X \in V \to ((x \in X \land y \in X) \to (\{x\} = \{y\} \leftrightarrow x = y))$
10	4 9	dom2lem	$⊢ X \in V \to (x \in X ⟼ \{x\}) : X \underset{1-1}{⟶} V$
11		f1f1orn	$⊢ (x \in X ⟼ \{x\}) : X \underset{1-1}{⟶} V \to (x \in X ⟼ \{x\}) : X \underset{1-1 onto}{⟶} ran (x \in X ⟼ \{x\})$
12	10 11	syl	$⊢ X \in V \to (x \in X ⟼ \{x\}) : X \underset{1-1 onto}{⟶} ran (x \in X ⟼ \{x\})$
13		f1oeng	$⊢ (X \in V \land (x \in X ⟼ \{x\}) : X \underset{1-1 onto}{⟶} ran (x \in X ⟼ \{x\})) \to X \approx ran (x \in X ⟼ \{x\})$
14	12 13	mpdan	$⊢ X \in V \to X \approx ran (x \in X ⟼ \{x\})$
15		domen1	$⊢ X \approx ran (x \in X ⟼ \{x\}) \to (X ≼ ω \leftrightarrow ran (x \in X ⟼ \{x\}) ≼ ω)$
16	14 15	syl	$⊢ X \in V \to (X ≼ ω \leftrightarrow ran (x \in X ⟼ \{x\}) ≼ ω)$
17		distop	$⊢ X \in V \to 𝒫 X \in Top$
18	5	snelpw	$⊢ x \in X \leftrightarrow \{x\} \in 𝒫 X$
19	18	bilani	$⊢ (X \in V \land x \in X) \to \{x\} \in 𝒫 X$
20	19	fmpttd	$⊢ X \in V \to (x \in X ⟼ \{x\}) : X ⟶ 𝒫 X$
21	20	frnd	$⊢ X \in V \to ran (x \in X ⟼ \{x\}) \subseteq 𝒫 X$
22		elpwi	$⊢ y \in 𝒫 X \to y \subseteq X$
23	22	ad2antrl	$⊢ (X \in V \land (y \in 𝒫 X \land z \in y)) \to y \subseteq X$
24		simprr	$⊢ (X \in V \land (y \in 𝒫 X \land z \in y)) \to z \in y$
25	23 24	sseldd	$⊢ (X \in V \land (y \in 𝒫 X \land z \in y)) \to z \in X$
26		eqidd	$⊢ (X \in V \land (y \in 𝒫 X \land z \in y)) \to \{z\} = \{z\}$
27		sneq	$⊢ x = z \to \{x\} = \{z\}$
28	27	rspceeqv	$⊢ (z \in X \land \{z\} = \{z\}) \to \exists x \in X \{z\} = \{x\}$
29	25 26 28	syl2anc	$⊢ (X \in V \land (y \in 𝒫 X \land z \in y)) \to \exists x \in X \{z\} = \{x\}$
30		vsnex	$⊢ \{z\} \in V$
31		eqid	$⊢ (x \in X ⟼ \{x\}) = (x \in X ⟼ \{x\})$
32	31	elrnmpt	$⊢ \{z\} \in V \to (\{z\} \in ran (x \in X ⟼ \{x\}) \leftrightarrow \exists x \in X \{z\} = \{x\})$
33	30 32	ax-mp	$⊢ \{z\} \in ran (x \in X ⟼ \{x\}) \leftrightarrow \exists x \in X \{z\} = \{x\}$
34	29 33	sylibr	$⊢ (X \in V \land (y \in 𝒫 X \land z \in y)) \to \{z\} \in ran (x \in X ⟼ \{x\})$
35		vsnid	$⊢ z \in \{z\}$
36	35	a1i	$⊢ (X \in V \land (y \in 𝒫 X \land z \in y)) \to z \in \{z\}$
37	24	snssd	$⊢ (X \in V \land (y \in 𝒫 X \land z \in y)) \to \{z\} \subseteq y$
38		eleq2	$⊢ w = \{z\} \to (z \in w \leftrightarrow z \in \{z\})$
39		sseq1	$⊢ w = \{z\} \to (w \subseteq y \leftrightarrow \{z\} \subseteq y)$
40	38 39	anbi12d	$⊢ w = \{z\} \to ((z \in w \land w \subseteq y) \leftrightarrow (z \in \{z\} \land \{z\} \subseteq y))$
41	40	rspcev	$⊢ (\{z\} \in ran (x \in X ⟼ \{x\}) \land (z \in \{z\} \land \{z\} \subseteq y)) \to \exists w \in ran (x \in X ⟼ \{x\}) (z \in w \land w \subseteq y)$
42	34 36 37 41	syl12anc	$⊢ (X \in V \land (y \in 𝒫 X \land z \in y)) \to \exists w \in ran (x \in X ⟼ \{x\}) (z \in w \land w \subseteq y)$
43	42	ralrimivva	$⊢ X \in V \to \forall y \in 𝒫 X \forall z \in y \exists w \in ran (x \in X ⟼ \{x\}) (z \in w \land w \subseteq y)$
44		basgen2	$⊢ (𝒫 X \in Top \land ran (x \in X ⟼ \{x\}) \subseteq 𝒫 X \land \forall y \in 𝒫 X \forall z \in y \exists w \in ran (x \in X ⟼ \{x\}) (z \in w \land w \subseteq y)) \to topGen (ran (x \in X ⟼ \{x\})) = 𝒫 X$
45	17 21 43 44	syl3anc	$⊢ X \in V \to topGen (ran (x \in X ⟼ \{x\})) = 𝒫 X$
46	45	adantr	$⊢ (X \in V \land ran (x \in X ⟼ \{x\}) ≼ ω) \to topGen (ran (x \in X ⟼ \{x\})) = 𝒫 X$
47	45 17	eqeltrd	$⊢ X \in V \to topGen (ran (x \in X ⟼ \{x\})) \in Top$
48		tgclb	$⊢ ran (x \in X ⟼ \{x\}) \in TopBases \leftrightarrow topGen (ran (x \in X ⟼ \{x\})) \in Top$
49	47 48	sylibr	$⊢ X \in V \to ran (x \in X ⟼ \{x\}) \in TopBases$
50		2ndci	$⊢ (ran (x \in X ⟼ \{x\}) \in TopBases \land ran (x \in X ⟼ \{x\}) ≼ ω) \to topGen (ran (x \in X ⟼ \{x\})) \in 2^{nd} 𝜔$
51	49 50	sylan	$⊢ (X \in V \land ran (x \in X ⟼ \{x\}) ≼ ω) \to topGen (ran (x \in X ⟼ \{x\})) \in 2^{nd} 𝜔$
52	46 51	eqeltrrd	$⊢ (X \in V \land ran (x \in X ⟼ \{x\}) ≼ ω) \to 𝒫 X \in 2^{nd} 𝜔$
53		is2ndc	$⊢ 𝒫 X \in 2^{nd} 𝜔 \leftrightarrow \exists b \in TopBases (b ≼ ω \land topGen (b) = 𝒫 X)$
54		vex	$⊢ b \in V$
55	18	bilani	$⊢ (((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \land x \in X) \to \{x\} \in 𝒫 X$
56		simplrr	$⊢ (((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \land x \in X) \to topGen (b) = 𝒫 X$
57	55 56	eleqtrrd	$⊢ (((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \land x \in X) \to \{x\} \in topGen (b)$
58		vsnid	$⊢ x \in \{x\}$
59		tg2	$⊢ (\{x\} \in topGen (b) \land x \in \{x\}) \to \exists y \in b (x \in y \land y \subseteq \{x\})$
60	57 58 59	sylancl	$⊢ (((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \land x \in X) \to \exists y \in b (x \in y \land y \subseteq \{x\})$
61		simprrl	$⊢ ((((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \land x \in X) \land (y \in b \land (x \in y \land y \subseteq \{x\}))) \to x \in y$
62	61	snssd	$⊢ ((((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \land x \in X) \land (y \in b \land (x \in y \land y \subseteq \{x\}))) \to \{x\} \subseteq y$
63		simprrr	$⊢ ((((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \land x \in X) \land (y \in b \land (x \in y \land y \subseteq \{x\}))) \to y \subseteq \{x\}$
64	62 63	eqssd	$⊢ ((((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \land x \in X) \land (y \in b \land (x \in y \land y \subseteq \{x\}))) \to \{x\} = y$
65		simprl	$⊢ ((((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \land x \in X) \land (y \in b \land (x \in y \land y \subseteq \{x\}))) \to y \in b$
66	64 65	eqeltrd	$⊢ ((((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \land x \in X) \land (y \in b \land (x \in y \land y \subseteq \{x\}))) \to \{x\} \in b$
67	60 66	rexlimddv	$⊢ (((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \land x \in X) \to \{x\} \in b$
68	67	fmpttd	$⊢ ((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \to (x \in X ⟼ \{x\}) : X ⟶ b$
69	68	frnd	$⊢ ((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \to ran (x \in X ⟼ \{x\}) \subseteq b$
70		ssdomg	$⊢ b \in V \to (ran (x \in X ⟼ \{x\}) \subseteq b \to ran (x \in X ⟼ \{x\}) ≼ b)$
71	54 69 70	mpsyl	$⊢ ((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \to ran (x \in X ⟼ \{x\}) ≼ b$
72		simprl	$⊢ ((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \to b ≼ ω$
73		domtr	$⊢ (ran (x \in X ⟼ \{x\}) ≼ b \land b ≼ ω) \to ran (x \in X ⟼ \{x\}) ≼ ω$
74	71 72 73	syl2anc	$⊢ ((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \to ran (x \in X ⟼ \{x\}) ≼ ω$
75	74	rexlimdva2	$⊢ X \in V \to (\exists b \in TopBases (b ≼ ω \land topGen (b) = 𝒫 X) \to ran (x \in X ⟼ \{x\}) ≼ ω)$
76	53 75	biimtrid	$⊢ X \in V \to (𝒫 X \in 2^{nd} 𝜔 \to ran (x \in X ⟼ \{x\}) ≼ ω)$
77	76	imp	$⊢ (X \in V \land 𝒫 X \in 2^{nd} 𝜔) \to ran (x \in X ⟼ \{x\}) ≼ ω$
78	52 77	impbida	$⊢ X \in V \to (ran (x \in X ⟼ \{x\}) ≼ ω \leftrightarrow 𝒫 X \in 2^{nd} 𝜔)$
79	16 78	bitrd	$⊢ X \in V \to (X ≼ ω \leftrightarrow 𝒫 X \in 2^{nd} 𝜔)$
80	1 2 79	pm5.21nii	$⊢ X ≼ ω \leftrightarrow 𝒫 X \in 2^{nd} 𝜔$

Metamath Proof Explorer

Theorem dis2ndc

Proof