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		snex	$⊢ \{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		simpr	$⊢ (X \in V \land x \in X) \to x \in X$
19	5	snelpw	$⊢ x \in X \leftrightarrow \{x\} \in 𝒫 X$
20	18 19	sylib	$⊢ (X \in V \land x \in X) \to \{x\} \in 𝒫 X$
21	20	fmpttd	$⊢ X \in V \to (x \in X ⟼ \{x\}) : X ⟶ 𝒫 X$
22	21	frnd	$⊢ X \in V \to ran (x \in X ⟼ \{x\}) \subseteq 𝒫 X$
23		elpwi	$⊢ y \in 𝒫 X \to y \subseteq X$
24	23	ad2antrl	$⊢ (X \in V \land (y \in 𝒫 X \land z \in y)) \to y \subseteq X$
25		simprr	$⊢ (X \in V \land (y \in 𝒫 X \land z \in y)) \to z \in y$
26	24 25	sseldd	$⊢ (X \in V \land (y \in 𝒫 X \land z \in y)) \to z \in X$
27		eqidd	$⊢ (X \in V \land (y \in 𝒫 X \land z \in y)) \to \{z\} = \{z\}$
28		sneq	$⊢ x = z \to \{x\} = \{z\}$
29	28	rspceeqv	$⊢ (z \in X \land \{z\} = \{z\}) \to \exists x \in X \{z\} = \{x\}$
30	26 27 29	syl2anc	$⊢ (X \in V \land (y \in 𝒫 X \land z \in y)) \to \exists x \in X \{z\} = \{x\}$
31		snex	$⊢ \{z\} \in V$
32		eqid	$⊢ (x \in X ⟼ \{x\}) = (x \in X ⟼ \{x\})$
33	32	elrnmpt	$⊢ \{z\} \in V \to (\{z\} \in ran (x \in X ⟼ \{x\}) \leftrightarrow \exists x \in X \{z\} = \{x\})$
34	31 33	ax-mp	$⊢ \{z\} \in ran (x \in X ⟼ \{x\}) \leftrightarrow \exists x \in X \{z\} = \{x\}$
35	30 34	sylibr	$⊢ (X \in V \land (y \in 𝒫 X \land z \in y)) \to \{z\} \in ran (x \in X ⟼ \{x\})$
36		vsnid	$⊢ z \in \{z\}$
37	36	a1i	$⊢ (X \in V \land (y \in 𝒫 X \land z \in y)) \to z \in \{z\}$
38	25	snssd	$⊢ (X \in V \land (y \in 𝒫 X \land z \in y)) \to \{z\} \subseteq y$
39		eleq2	$⊢ w = \{z\} \to (z \in w \leftrightarrow z \in \{z\})$
40		sseq1	$⊢ w = \{z\} \to (w \subseteq y \leftrightarrow \{z\} \subseteq y)$
41	39 40	anbi12d	$⊢ w = \{z\} \to ((z \in w \land w \subseteq y) \leftrightarrow (z \in \{z\} \land \{z\} \subseteq y))$
42	41	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)$
43	35 37 38 42	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)$
44	43	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)$
45		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$
46	17 22 44 45	syl3anc	$⊢ X \in V \to topGen (ran (x \in X ⟼ \{x\})) = 𝒫 X$
47	46	adantr	$⊢ (X \in V \land ran (x \in X ⟼ \{x\}) ≼ ω) \to topGen (ran (x \in X ⟼ \{x\})) = 𝒫 X$
48	46 17	eqeltrd	$⊢ X \in V \to topGen (ran (x \in X ⟼ \{x\})) \in Top$
49		tgclb	$⊢ ran (x \in X ⟼ \{x\}) \in TopBases \leftrightarrow topGen (ran (x \in X ⟼ \{x\})) \in Top$
50	48 49	sylibr	$⊢ X \in V \to ran (x \in X ⟼ \{x\}) \in TopBases$
51		2ndci	$⊢ (ran (x \in X ⟼ \{x\}) \in TopBases \land ran (x \in X ⟼ \{x\}) ≼ ω) \to topGen (ran (x \in X ⟼ \{x\})) \in 2^{nd} 𝜔$
52	50 51	sylan	$⊢ (X \in V \land ran (x \in X ⟼ \{x\}) ≼ ω) \to topGen (ran (x \in X ⟼ \{x\})) \in 2^{nd} 𝜔$
53	47 52	eqeltrrd	$⊢ (X \in V \land ran (x \in X ⟼ \{x\}) ≼ ω) \to 𝒫 X \in 2^{nd} 𝜔$
54		is2ndc	$⊢ 𝒫 X \in 2^{nd} 𝜔 \leftrightarrow \exists b \in TopBases (b ≼ ω \land topGen (b) = 𝒫 X)$
55		vex	$⊢ b \in V$
56		simpr	$⊢ (((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \land x \in X) \to x \in X$
57	56 19	sylib	$⊢ (((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \land x \in X) \to \{x\} \in 𝒫 X$
58		simplrr	$⊢ (((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \land x \in X) \to topGen (b) = 𝒫 X$
59	57 58	eleqtrrd	$⊢ (((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \land x \in X) \to \{x\} \in topGen (b)$
60		vsnid	$⊢ x \in \{x\}$
61		tg2	$⊢ (\{x\} \in topGen (b) \land x \in \{x\}) \to \exists y \in b (x \in y \land y \subseteq \{x\})$
62	59 60 61	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\})$
63		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$
64	63	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$
65		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\}$
66	64 65	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$
67		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$
68	66 67	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$
69	62 68	rexlimddv	$⊢ (((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \land x \in X) \to \{x\} \in b$
70	69	fmpttd	$⊢ ((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \to (x \in X ⟼ \{x\}) : X ⟶ b$
71	70	frnd	$⊢ ((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \to ran (x \in X ⟼ \{x\}) \subseteq b$
72		ssdomg	$⊢ b \in V \to (ran (x \in X ⟼ \{x\}) \subseteq b \to ran (x \in X ⟼ \{x\}) ≼ b)$
73	55 71 72	mpsyl	$⊢ ((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \to ran (x \in X ⟼ \{x\}) ≼ b$
74		simprl	$⊢ ((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \to b ≼ ω$
75		domtr	$⊢ (ran (x \in X ⟼ \{x\}) ≼ b \land b ≼ ω) \to ran (x \in X ⟼ \{x\}) ≼ ω$
76	73 74 75	syl2anc	$⊢ ((X \in V \land b \in TopBases) \land (b ≼ ω \land topGen (b) = 𝒫 X)) \to ran (x \in X ⟼ \{x\}) ≼ ω$
77	76	rexlimdva2	$⊢ X \in V \to (\exists b \in TopBases (b ≼ ω \land topGen (b) = 𝒫 X) \to ran (x \in X ⟼ \{x\}) ≼ ω)$
78	54 77	syl5bi	$⊢ X \in V \to (𝒫 X \in 2^{nd} 𝜔 \to ran (x \in X ⟼ \{x\}) ≼ ω)$
79	78	imp	$⊢ (X \in V \land 𝒫 X \in 2^{nd} 𝜔) \to ran (x \in X ⟼ \{x\}) ≼ ω$
80	53 79	impbida	$⊢ X \in V \to (ran (x \in X ⟼ \{x\}) ≼ ω \leftrightarrow 𝒫 X \in 2^{nd} 𝜔)$
81	16 80	bitrd	$⊢ X \in V \to (X ≼ ω \leftrightarrow 𝒫 X \in 2^{nd} 𝜔)$
82	1 2 81	pm5.21nii	$⊢ X ≼ ω \leftrightarrow 𝒫 X \in 2^{nd} 𝜔$

Metamath Proof Explorer

Theorem dis2ndc

Proof