MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dis2ndc Structured version   Visualization version   GIF version

Theorem dis2ndc 21073
Description: A discrete space is second-countable iff it is countable. (Contributed by Mario Carneiro, 13-Apr-2015.)
Assertion
Ref Expression
dis2ndc (𝑋 ≼ ω ↔ 𝒫 𝑋 ∈ 2nd𝜔)

Proof of Theorem dis2ndc
Dummy variables 𝑤 𝑏 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reldom 7847 . . 3 Rel ≼
21brrelexi 5082 . 2 (𝑋 ≼ ω → 𝑋 ∈ V)
3 elex 3185 . . 3 (𝒫 𝑋 ∈ 2nd𝜔 → 𝒫 𝑋 ∈ V)
4 pwexb 6867 . . 3 (𝑋 ∈ V ↔ 𝒫 𝑋 ∈ V)
53, 4sylibr 223 . 2 (𝒫 𝑋 ∈ 2nd𝜔 → 𝑋 ∈ V)
6 elex 3185 . . . . 5 (𝑋 ∈ V → 𝑋 ∈ V)
7 snex 4835 . . . . . . . 8 {𝑥} ∈ V
872a1i 12 . . . . . . 7 (𝑋 ∈ V → (𝑥𝑋 → {𝑥} ∈ V))
9 vex 3176 . . . . . . . . . 10 𝑥 ∈ V
109sneqr 4311 . . . . . . . . 9 ({𝑥} = {𝑦} → 𝑥 = 𝑦)
11 sneq 4135 . . . . . . . . 9 (𝑥 = 𝑦 → {𝑥} = {𝑦})
1210, 11impbii 198 . . . . . . . 8 ({𝑥} = {𝑦} ↔ 𝑥 = 𝑦)
13122a1i 12 . . . . . . 7 (𝑋 ∈ V → ((𝑥𝑋𝑦𝑋) → ({𝑥} = {𝑦} ↔ 𝑥 = 𝑦)))
148, 13dom2lem 7881 . . . . . 6 (𝑋 ∈ V → (𝑥𝑋 ↦ {𝑥}):𝑋1-1→V)
15 f1f1orn 6061 . . . . . 6 ((𝑥𝑋 ↦ {𝑥}):𝑋1-1→V → (𝑥𝑋 ↦ {𝑥}):𝑋1-1-onto→ran (𝑥𝑋 ↦ {𝑥}))
1614, 15syl 17 . . . . 5 (𝑋 ∈ V → (𝑥𝑋 ↦ {𝑥}):𝑋1-1-onto→ran (𝑥𝑋 ↦ {𝑥}))
17 f1oeng 7860 . . . . 5 ((𝑋 ∈ V ∧ (𝑥𝑋 ↦ {𝑥}):𝑋1-1-onto→ran (𝑥𝑋 ↦ {𝑥})) → 𝑋 ≈ ran (𝑥𝑋 ↦ {𝑥}))
186, 16, 17syl2anc 691 . . . 4 (𝑋 ∈ V → 𝑋 ≈ ran (𝑥𝑋 ↦ {𝑥}))
19 domen1 7987 . . . 4 (𝑋 ≈ ran (𝑥𝑋 ↦ {𝑥}) → (𝑋 ≼ ω ↔ ran (𝑥𝑋 ↦ {𝑥}) ≼ ω))
2018, 19syl 17 . . 3 (𝑋 ∈ V → (𝑋 ≼ ω ↔ ran (𝑥𝑋 ↦ {𝑥}) ≼ ω))
21 distop 20610 . . . . . . 7 (𝑋 ∈ V → 𝒫 𝑋 ∈ Top)
22 simpr 476 . . . . . . . . . 10 ((𝑋 ∈ V ∧ 𝑥𝑋) → 𝑥𝑋)
239snelpw 4840 . . . . . . . . . 10 (𝑥𝑋 ↔ {𝑥} ∈ 𝒫 𝑋)
2422, 23sylib 207 . . . . . . . . 9 ((𝑋 ∈ V ∧ 𝑥𝑋) → {𝑥} ∈ 𝒫 𝑋)
25 eqid 2610 . . . . . . . . 9 (𝑥𝑋 ↦ {𝑥}) = (𝑥𝑋 ↦ {𝑥})
2624, 25fmptd 6292 . . . . . . . 8 (𝑋 ∈ V → (𝑥𝑋 ↦ {𝑥}):𝑋⟶𝒫 𝑋)
27 frn 5966 . . . . . . . 8 ((𝑥𝑋 ↦ {𝑥}):𝑋⟶𝒫 𝑋 → ran (𝑥𝑋 ↦ {𝑥}) ⊆ 𝒫 𝑋)
2826, 27syl 17 . . . . . . 7 (𝑋 ∈ V → ran (𝑥𝑋 ↦ {𝑥}) ⊆ 𝒫 𝑋)
29 elpwi 4117 . . . . . . . . . . . . 13 (𝑦 ∈ 𝒫 𝑋𝑦𝑋)
3029ad2antrl 760 . . . . . . . . . . . 12 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → 𝑦𝑋)
31 simprr 792 . . . . . . . . . . . 12 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → 𝑧𝑦)
3230, 31sseldd 3569 . . . . . . . . . . 11 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → 𝑧𝑋)
33 eqidd 2611 . . . . . . . . . . 11 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → {𝑧} = {𝑧})
34 sneq 4135 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → {𝑥} = {𝑧})
3534eqeq2d 2620 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ({𝑧} = {𝑥} ↔ {𝑧} = {𝑧}))
3635rspcev 3282 . . . . . . . . . . 11 ((𝑧𝑋 ∧ {𝑧} = {𝑧}) → ∃𝑥𝑋 {𝑧} = {𝑥})
3732, 33, 36syl2anc 691 . . . . . . . . . 10 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → ∃𝑥𝑋 {𝑧} = {𝑥})
38 snex 4835 . . . . . . . . . . 11 {𝑧} ∈ V
3925elrnmpt 5293 . . . . . . . . . . 11 ({𝑧} ∈ V → ({𝑧} ∈ ran (𝑥𝑋 ↦ {𝑥}) ↔ ∃𝑥𝑋 {𝑧} = {𝑥}))
4038, 39ax-mp 5 . . . . . . . . . 10 ({𝑧} ∈ ran (𝑥𝑋 ↦ {𝑥}) ↔ ∃𝑥𝑋 {𝑧} = {𝑥})
4137, 40sylibr 223 . . . . . . . . 9 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → {𝑧} ∈ ran (𝑥𝑋 ↦ {𝑥}))
42 vsnid 4156 . . . . . . . . . 10 𝑧 ∈ {𝑧}
4342a1i 11 . . . . . . . . 9 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → 𝑧 ∈ {𝑧})
4431snssd 4281 . . . . . . . . 9 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → {𝑧} ⊆ 𝑦)
45 eleq2 2677 . . . . . . . . . . 11 (𝑤 = {𝑧} → (𝑧𝑤𝑧 ∈ {𝑧}))
46 sseq1 3589 . . . . . . . . . . 11 (𝑤 = {𝑧} → (𝑤𝑦 ↔ {𝑧} ⊆ 𝑦))
4745, 46anbi12d 743 . . . . . . . . . 10 (𝑤 = {𝑧} → ((𝑧𝑤𝑤𝑦) ↔ (𝑧 ∈ {𝑧} ∧ {𝑧} ⊆ 𝑦)))
4847rspcev 3282 . . . . . . . . 9 (({𝑧} ∈ ran (𝑥𝑋 ↦ {𝑥}) ∧ (𝑧 ∈ {𝑧} ∧ {𝑧} ⊆ 𝑦)) → ∃𝑤 ∈ ran (𝑥𝑋 ↦ {𝑥})(𝑧𝑤𝑤𝑦))
4941, 43, 44, 48syl12anc 1316 . . . . . . . 8 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → ∃𝑤 ∈ ran (𝑥𝑋 ↦ {𝑥})(𝑧𝑤𝑤𝑦))
5049ralrimivva 2954 . . . . . . 7 (𝑋 ∈ V → ∀𝑦 ∈ 𝒫 𝑋𝑧𝑦𝑤 ∈ ran (𝑥𝑋 ↦ {𝑥})(𝑧𝑤𝑤𝑦))
51 basgen2 20604 . . . . . . 7 ((𝒫 𝑋 ∈ Top ∧ ran (𝑥𝑋 ↦ {𝑥}) ⊆ 𝒫 𝑋 ∧ ∀𝑦 ∈ 𝒫 𝑋𝑧𝑦𝑤 ∈ ran (𝑥𝑋 ↦ {𝑥})(𝑧𝑤𝑤𝑦)) → (topGen‘ran (𝑥𝑋 ↦ {𝑥})) = 𝒫 𝑋)
5221, 28, 50, 51syl3anc 1318 . . . . . 6 (𝑋 ∈ V → (topGen‘ran (𝑥𝑋 ↦ {𝑥})) = 𝒫 𝑋)
5352adantr 480 . . . . 5 ((𝑋 ∈ V ∧ ran (𝑥𝑋 ↦ {𝑥}) ≼ ω) → (topGen‘ran (𝑥𝑋 ↦ {𝑥})) = 𝒫 𝑋)
5452, 21eqeltrd 2688 . . . . . . 7 (𝑋 ∈ V → (topGen‘ran (𝑥𝑋 ↦ {𝑥})) ∈ Top)
55 tgclb 20585 . . . . . . 7 (ran (𝑥𝑋 ↦ {𝑥}) ∈ TopBases ↔ (topGen‘ran (𝑥𝑋 ↦ {𝑥})) ∈ Top)
5654, 55sylibr 223 . . . . . 6 (𝑋 ∈ V → ran (𝑥𝑋 ↦ {𝑥}) ∈ TopBases)
57 2ndci 21061 . . . . . 6 ((ran (𝑥𝑋 ↦ {𝑥}) ∈ TopBases ∧ ran (𝑥𝑋 ↦ {𝑥}) ≼ ω) → (topGen‘ran (𝑥𝑋 ↦ {𝑥})) ∈ 2nd𝜔)
5856, 57sylan 487 . . . . 5 ((𝑋 ∈ V ∧ ran (𝑥𝑋 ↦ {𝑥}) ≼ ω) → (topGen‘ran (𝑥𝑋 ↦ {𝑥})) ∈ 2nd𝜔)
5953, 58eqeltrrd 2689 . . . 4 ((𝑋 ∈ V ∧ ran (𝑥𝑋 ↦ {𝑥}) ≼ ω) → 𝒫 𝑋 ∈ 2nd𝜔)
60 is2ndc 21059 . . . . . 6 (𝒫 𝑋 ∈ 2nd𝜔 ↔ ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋))
61 vex 3176 . . . . . . . . . 10 𝑏 ∈ V
62 simpr 476 . . . . . . . . . . . . . . . 16 ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) → 𝑥𝑋)
6362, 23sylib 207 . . . . . . . . . . . . . . 15 ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) → {𝑥} ∈ 𝒫 𝑋)
64 simplrr 797 . . . . . . . . . . . . . . 15 ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) → (topGen‘𝑏) = 𝒫 𝑋)
6563, 64eleqtrrd 2691 . . . . . . . . . . . . . 14 ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) → {𝑥} ∈ (topGen‘𝑏))
66 vsnid 4156 . . . . . . . . . . . . . 14 𝑥 ∈ {𝑥}
67 tg2 20580 . . . . . . . . . . . . . 14 (({𝑥} ∈ (topGen‘𝑏) ∧ 𝑥 ∈ {𝑥}) → ∃𝑦𝑏 (𝑥𝑦𝑦 ⊆ {𝑥}))
6865, 66, 67sylancl 693 . . . . . . . . . . . . 13 ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) → ∃𝑦𝑏 (𝑥𝑦𝑦 ⊆ {𝑥}))
69 simprrl 800 . . . . . . . . . . . . . . . 16 (((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) ∧ (𝑦𝑏 ∧ (𝑥𝑦𝑦 ⊆ {𝑥}))) → 𝑥𝑦)
7069snssd 4281 . . . . . . . . . . . . . . 15 (((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) ∧ (𝑦𝑏 ∧ (𝑥𝑦𝑦 ⊆ {𝑥}))) → {𝑥} ⊆ 𝑦)
71 simprrr 801 . . . . . . . . . . . . . . 15 (((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) ∧ (𝑦𝑏 ∧ (𝑥𝑦𝑦 ⊆ {𝑥}))) → 𝑦 ⊆ {𝑥})
7270, 71eqssd 3585 . . . . . . . . . . . . . 14 (((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) ∧ (𝑦𝑏 ∧ (𝑥𝑦𝑦 ⊆ {𝑥}))) → {𝑥} = 𝑦)
73 simprl 790 . . . . . . . . . . . . . 14 (((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) ∧ (𝑦𝑏 ∧ (𝑥𝑦𝑦 ⊆ {𝑥}))) → 𝑦𝑏)
7472, 73eqeltrd 2688 . . . . . . . . . . . . 13 (((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) ∧ (𝑦𝑏 ∧ (𝑥𝑦𝑦 ⊆ {𝑥}))) → {𝑥} ∈ 𝑏)
7568, 74rexlimddv 3017 . . . . . . . . . . . 12 ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) → {𝑥} ∈ 𝑏)
7675, 25fmptd 6292 . . . . . . . . . . 11 (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) → (𝑥𝑋 ↦ {𝑥}):𝑋𝑏)
77 frn 5966 . . . . . . . . . . 11 ((𝑥𝑋 ↦ {𝑥}):𝑋𝑏 → ran (𝑥𝑋 ↦ {𝑥}) ⊆ 𝑏)
7876, 77syl 17 . . . . . . . . . 10 (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) → ran (𝑥𝑋 ↦ {𝑥}) ⊆ 𝑏)
79 ssdomg 7887 . . . . . . . . . 10 (𝑏 ∈ V → (ran (𝑥𝑋 ↦ {𝑥}) ⊆ 𝑏 → ran (𝑥𝑋 ↦ {𝑥}) ≼ 𝑏))
8061, 78, 79mpsyl 66 . . . . . . . . 9 (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) → ran (𝑥𝑋 ↦ {𝑥}) ≼ 𝑏)
81 simprl 790 . . . . . . . . 9 (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) → 𝑏 ≼ ω)
82 domtr 7895 . . . . . . . . 9 ((ran (𝑥𝑋 ↦ {𝑥}) ≼ 𝑏𝑏 ≼ ω) → ran (𝑥𝑋 ↦ {𝑥}) ≼ ω)
8380, 81, 82syl2anc 691 . . . . . . . 8 (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) → ran (𝑥𝑋 ↦ {𝑥}) ≼ ω)
8483ex 449 . . . . . . 7 ((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) → ((𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋) → ran (𝑥𝑋 ↦ {𝑥}) ≼ ω))
8584rexlimdva 3013 . . . . . 6 (𝑋 ∈ V → (∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋) → ran (𝑥𝑋 ↦ {𝑥}) ≼ ω))
8660, 85syl5bi 231 . . . . 5 (𝑋 ∈ V → (𝒫 𝑋 ∈ 2nd𝜔 → ran (𝑥𝑋 ↦ {𝑥}) ≼ ω))
8786imp 444 . . . 4 ((𝑋 ∈ V ∧ 𝒫 𝑋 ∈ 2nd𝜔) → ran (𝑥𝑋 ↦ {𝑥}) ≼ ω)
8859, 87impbida 873 . . 3 (𝑋 ∈ V → (ran (𝑥𝑋 ↦ {𝑥}) ≼ ω ↔ 𝒫 𝑋 ∈ 2nd𝜔))
8920, 88bitrd 267 . 2 (𝑋 ∈ V → (𝑋 ≼ ω ↔ 𝒫 𝑋 ∈ 2nd𝜔))
902, 5, 89pm5.21nii 367 1 (𝑋 ≼ ω ↔ 𝒫 𝑋 ∈ 2nd𝜔)
Colors of variables: wff setvar class
Syntax hints:  wb 195  wa 383   = wceq 1475  wcel 1977  wral 2896  wrex 2897  Vcvv 3173  wss 3540  𝒫 cpw 4108  {csn 4125   class class class wbr 4583  cmpt 4643  ran crn 5039  wf 5800  1-1wf1 5801  1-1-ontowf1o 5803  cfv 5804  ωcom 6957  cen 7838  cdom 7839  topGenctg 15921  Topctop 20517  TopBasesctb 20520  2nd𝜔c2ndc 21051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-er 7629  df-en 7842  df-dom 7843  df-topgen 15927  df-top 20521  df-bases 20522  df-2ndc 21053
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator