# Metamath Proof Explorer

## Theorem dis2ndc

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

Ref Expression
Assertion dis2ndc ${⊢}{X}\preccurlyeq \mathrm{\omega }↔𝒫{X}\in {2}^{nd}𝜔$

### Proof

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