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

Theorem dis2ndc 21386
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 8078 . . 3 Rel ≼
21brrelexi 5267 . 2 (𝑋 ≼ ω → 𝑋 ∈ V)
3 pwexr 7091 . 2 (𝒫 𝑋 ∈ 2nd𝜔 → 𝑋 ∈ V)
4 elex 3316 . . . . 5 (𝑋 ∈ V → 𝑋 ∈ V)
5 snex 5013 . . . . . . . 8 {𝑥} ∈ V
652a1i 12 . . . . . . 7 (𝑋 ∈ V → (𝑥𝑋 → {𝑥} ∈ V))
7 vex 3307 . . . . . . . . . 10 𝑥 ∈ V
87sneqr 4479 . . . . . . . . 9 ({𝑥} = {𝑦} → 𝑥 = 𝑦)
9 sneq 4295 . . . . . . . . 9 (𝑥 = 𝑦 → {𝑥} = {𝑦})
108, 9impbii 199 . . . . . . . 8 ({𝑥} = {𝑦} ↔ 𝑥 = 𝑦)
11102a1i 12 . . . . . . 7 (𝑋 ∈ V → ((𝑥𝑋𝑦𝑋) → ({𝑥} = {𝑦} ↔ 𝑥 = 𝑦)))
126, 11dom2lem 8112 . . . . . 6 (𝑋 ∈ V → (𝑥𝑋 ↦ {𝑥}):𝑋1-1→V)
13 f1f1orn 6261 . . . . . 6 ((𝑥𝑋 ↦ {𝑥}):𝑋1-1→V → (𝑥𝑋 ↦ {𝑥}):𝑋1-1-onto→ran (𝑥𝑋 ↦ {𝑥}))
1412, 13syl 17 . . . . 5 (𝑋 ∈ V → (𝑥𝑋 ↦ {𝑥}):𝑋1-1-onto→ran (𝑥𝑋 ↦ {𝑥}))
15 f1oeng 8091 . . . . 5 ((𝑋 ∈ V ∧ (𝑥𝑋 ↦ {𝑥}):𝑋1-1-onto→ran (𝑥𝑋 ↦ {𝑥})) → 𝑋 ≈ ran (𝑥𝑋 ↦ {𝑥}))
164, 14, 15syl2anc 696 . . . 4 (𝑋 ∈ V → 𝑋 ≈ ran (𝑥𝑋 ↦ {𝑥}))
17 domen1 8218 . . . 4 (𝑋 ≈ ran (𝑥𝑋 ↦ {𝑥}) → (𝑋 ≼ ω ↔ ran (𝑥𝑋 ↦ {𝑥}) ≼ ω))
1816, 17syl 17 . . 3 (𝑋 ∈ V → (𝑋 ≼ ω ↔ ran (𝑥𝑋 ↦ {𝑥}) ≼ ω))
19 distop 20922 . . . . . . 7 (𝑋 ∈ V → 𝒫 𝑋 ∈ Top)
20 simpr 479 . . . . . . . . . 10 ((𝑋 ∈ V ∧ 𝑥𝑋) → 𝑥𝑋)
217snelpw 5018 . . . . . . . . . 10 (𝑥𝑋 ↔ {𝑥} ∈ 𝒫 𝑋)
2220, 21sylib 208 . . . . . . . . 9 ((𝑋 ∈ V ∧ 𝑥𝑋) → {𝑥} ∈ 𝒫 𝑋)
23 eqid 2724 . . . . . . . . 9 (𝑥𝑋 ↦ {𝑥}) = (𝑥𝑋 ↦ {𝑥})
2422, 23fmptd 6500 . . . . . . . 8 (𝑋 ∈ V → (𝑥𝑋 ↦ {𝑥}):𝑋⟶𝒫 𝑋)
25 frn 6166 . . . . . . . 8 ((𝑥𝑋 ↦ {𝑥}):𝑋⟶𝒫 𝑋 → ran (𝑥𝑋 ↦ {𝑥}) ⊆ 𝒫 𝑋)
2624, 25syl 17 . . . . . . 7 (𝑋 ∈ V → ran (𝑥𝑋 ↦ {𝑥}) ⊆ 𝒫 𝑋)
27 elpwi 4276 . . . . . . . . . . . . 13 (𝑦 ∈ 𝒫 𝑋𝑦𝑋)
2827ad2antrl 766 . . . . . . . . . . . 12 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → 𝑦𝑋)
29 simprr 813 . . . . . . . . . . . 12 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → 𝑧𝑦)
3028, 29sseldd 3710 . . . . . . . . . . 11 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → 𝑧𝑋)
31 eqidd 2725 . . . . . . . . . . 11 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → {𝑧} = {𝑧})
32 sneq 4295 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → {𝑥} = {𝑧})
3332eqeq2d 2734 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ({𝑧} = {𝑥} ↔ {𝑧} = {𝑧}))
3433rspcev 3413 . . . . . . . . . . 11 ((𝑧𝑋 ∧ {𝑧} = {𝑧}) → ∃𝑥𝑋 {𝑧} = {𝑥})
3530, 31, 34syl2anc 696 . . . . . . . . . 10 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → ∃𝑥𝑋 {𝑧} = {𝑥})
36 snex 5013 . . . . . . . . . . 11 {𝑧} ∈ V
3723elrnmpt 5479 . . . . . . . . . . 11 ({𝑧} ∈ V → ({𝑧} ∈ ran (𝑥𝑋 ↦ {𝑥}) ↔ ∃𝑥𝑋 {𝑧} = {𝑥}))
3836, 37ax-mp 5 . . . . . . . . . 10 ({𝑧} ∈ ran (𝑥𝑋 ↦ {𝑥}) ↔ ∃𝑥𝑋 {𝑧} = {𝑥})
3935, 38sylibr 224 . . . . . . . . 9 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → {𝑧} ∈ ran (𝑥𝑋 ↦ {𝑥}))
40 vsnid 4317 . . . . . . . . . 10 𝑧 ∈ {𝑧}
4140a1i 11 . . . . . . . . 9 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → 𝑧 ∈ {𝑧})
4229snssd 4448 . . . . . . . . 9 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → {𝑧} ⊆ 𝑦)
43 eleq2 2792 . . . . . . . . . . 11 (𝑤 = {𝑧} → (𝑧𝑤𝑧 ∈ {𝑧}))
44 sseq1 3732 . . . . . . . . . . 11 (𝑤 = {𝑧} → (𝑤𝑦 ↔ {𝑧} ⊆ 𝑦))
4543, 44anbi12d 749 . . . . . . . . . 10 (𝑤 = {𝑧} → ((𝑧𝑤𝑤𝑦) ↔ (𝑧 ∈ {𝑧} ∧ {𝑧} ⊆ 𝑦)))
4645rspcev 3413 . . . . . . . . 9 (({𝑧} ∈ ran (𝑥𝑋 ↦ {𝑥}) ∧ (𝑧 ∈ {𝑧} ∧ {𝑧} ⊆ 𝑦)) → ∃𝑤 ∈ ran (𝑥𝑋 ↦ {𝑥})(𝑧𝑤𝑤𝑦))
4739, 41, 42, 46syl12anc 1437 . . . . . . . 8 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → ∃𝑤 ∈ ran (𝑥𝑋 ↦ {𝑥})(𝑧𝑤𝑤𝑦))
4847ralrimivva 3073 . . . . . . 7 (𝑋 ∈ V → ∀𝑦 ∈ 𝒫 𝑋𝑧𝑦𝑤 ∈ ran (𝑥𝑋 ↦ {𝑥})(𝑧𝑤𝑤𝑦))
49 basgen2 20916 . . . . . . 7 ((𝒫 𝑋 ∈ Top ∧ ran (𝑥𝑋 ↦ {𝑥}) ⊆ 𝒫 𝑋 ∧ ∀𝑦 ∈ 𝒫 𝑋𝑧𝑦𝑤 ∈ ran (𝑥𝑋 ↦ {𝑥})(𝑧𝑤𝑤𝑦)) → (topGen‘ran (𝑥𝑋 ↦ {𝑥})) = 𝒫 𝑋)
5019, 26, 48, 49syl3anc 1439 . . . . . 6 (𝑋 ∈ V → (topGen‘ran (𝑥𝑋 ↦ {𝑥})) = 𝒫 𝑋)
5150adantr 472 . . . . 5 ((𝑋 ∈ V ∧ ran (𝑥𝑋 ↦ {𝑥}) ≼ ω) → (topGen‘ran (𝑥𝑋 ↦ {𝑥})) = 𝒫 𝑋)
5250, 19eqeltrd 2803 . . . . . . 7 (𝑋 ∈ V → (topGen‘ran (𝑥𝑋 ↦ {𝑥})) ∈ Top)
53 tgclb 20897 . . . . . . 7 (ran (𝑥𝑋 ↦ {𝑥}) ∈ TopBases ↔ (topGen‘ran (𝑥𝑋 ↦ {𝑥})) ∈ Top)
5452, 53sylibr 224 . . . . . 6 (𝑋 ∈ V → ran (𝑥𝑋 ↦ {𝑥}) ∈ TopBases)
55 2ndci 21374 . . . . . 6 ((ran (𝑥𝑋 ↦ {𝑥}) ∈ TopBases ∧ ran (𝑥𝑋 ↦ {𝑥}) ≼ ω) → (topGen‘ran (𝑥𝑋 ↦ {𝑥})) ∈ 2nd𝜔)
5654, 55sylan 489 . . . . 5 ((𝑋 ∈ V ∧ ran (𝑥𝑋 ↦ {𝑥}) ≼ ω) → (topGen‘ran (𝑥𝑋 ↦ {𝑥})) ∈ 2nd𝜔)
5751, 56eqeltrrd 2804 . . . 4 ((𝑋 ∈ V ∧ ran (𝑥𝑋 ↦ {𝑥}) ≼ ω) → 𝒫 𝑋 ∈ 2nd𝜔)
58 is2ndc 21372 . . . . . 6 (𝒫 𝑋 ∈ 2nd𝜔 ↔ ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋))
59 vex 3307 . . . . . . . . . 10 𝑏 ∈ V
60 simpr 479 . . . . . . . . . . . . . . . 16 ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) → 𝑥𝑋)
6160, 21sylib 208 . . . . . . . . . . . . . . 15 ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) → {𝑥} ∈ 𝒫 𝑋)
62 simplrr 820 . . . . . . . . . . . . . . 15 ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) → (topGen‘𝑏) = 𝒫 𝑋)
6361, 62eleqtrrd 2806 . . . . . . . . . . . . . 14 ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) → {𝑥} ∈ (topGen‘𝑏))
64 vsnid 4317 . . . . . . . . . . . . . 14 𝑥 ∈ {𝑥}
65 tg2 20892 . . . . . . . . . . . . . 14 (({𝑥} ∈ (topGen‘𝑏) ∧ 𝑥 ∈ {𝑥}) → ∃𝑦𝑏 (𝑥𝑦𝑦 ⊆ {𝑥}))
6663, 64, 65sylancl 697 . . . . . . . . . . . . 13 ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) → ∃𝑦𝑏 (𝑥𝑦𝑦 ⊆ {𝑥}))
67 simprrl 823 . . . . . . . . . . . . . . . 16 (((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) ∧ (𝑦𝑏 ∧ (𝑥𝑦𝑦 ⊆ {𝑥}))) → 𝑥𝑦)
6867snssd 4448 . . . . . . . . . . . . . . 15 (((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) ∧ (𝑦𝑏 ∧ (𝑥𝑦𝑦 ⊆ {𝑥}))) → {𝑥} ⊆ 𝑦)
69 simprrr 824 . . . . . . . . . . . . . . 15 (((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) ∧ (𝑦𝑏 ∧ (𝑥𝑦𝑦 ⊆ {𝑥}))) → 𝑦 ⊆ {𝑥})
7068, 69eqssd 3726 . . . . . . . . . . . . . 14 (((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) ∧ (𝑦𝑏 ∧ (𝑥𝑦𝑦 ⊆ {𝑥}))) → {𝑥} = 𝑦)
71 simprl 811 . . . . . . . . . . . . . 14 (((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) ∧ (𝑦𝑏 ∧ (𝑥𝑦𝑦 ⊆ {𝑥}))) → 𝑦𝑏)
7270, 71eqeltrd 2803 . . . . . . . . . . . . 13 (((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) ∧ (𝑦𝑏 ∧ (𝑥𝑦𝑦 ⊆ {𝑥}))) → {𝑥} ∈ 𝑏)
7366, 72rexlimddv 3137 . . . . . . . . . . . 12 ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) → {𝑥} ∈ 𝑏)
7473, 23fmptd 6500 . . . . . . . . . . 11 (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) → (𝑥𝑋 ↦ {𝑥}):𝑋𝑏)
75 frn 6166 . . . . . . . . . . 11 ((𝑥𝑋 ↦ {𝑥}):𝑋𝑏 → ran (𝑥𝑋 ↦ {𝑥}) ⊆ 𝑏)
7674, 75syl 17 . . . . . . . . . 10 (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) → ran (𝑥𝑋 ↦ {𝑥}) ⊆ 𝑏)
77 ssdomg 8118 . . . . . . . . . 10 (𝑏 ∈ V → (ran (𝑥𝑋 ↦ {𝑥}) ⊆ 𝑏 → ran (𝑥𝑋 ↦ {𝑥}) ≼ 𝑏))
7859, 76, 77mpsyl 68 . . . . . . . . 9 (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) → ran (𝑥𝑋 ↦ {𝑥}) ≼ 𝑏)
79 simprl 811 . . . . . . . . 9 (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) → 𝑏 ≼ ω)
80 domtr 8125 . . . . . . . . 9 ((ran (𝑥𝑋 ↦ {𝑥}) ≼ 𝑏𝑏 ≼ ω) → ran (𝑥𝑋 ↦ {𝑥}) ≼ ω)
8178, 79, 80syl2anc 696 . . . . . . . 8 (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) → ran (𝑥𝑋 ↦ {𝑥}) ≼ ω)
8281ex 449 . . . . . . 7 ((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) → ((𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋) → ran (𝑥𝑋 ↦ {𝑥}) ≼ ω))
8382rexlimdva 3133 . . . . . 6 (𝑋 ∈ V → (∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋) → ran (𝑥𝑋 ↦ {𝑥}) ≼ ω))
8458, 83syl5bi 232 . . . . 5 (𝑋 ∈ V → (𝒫 𝑋 ∈ 2nd𝜔 → ran (𝑥𝑋 ↦ {𝑥}) ≼ ω))
8584imp 444 . . . 4 ((𝑋 ∈ V ∧ 𝒫 𝑋 ∈ 2nd𝜔) → ran (𝑥𝑋 ↦ {𝑥}) ≼ ω)
8657, 85impbida 913 . . 3 (𝑋 ∈ V → (ran (𝑥𝑋 ↦ {𝑥}) ≼ ω ↔ 𝒫 𝑋 ∈ 2nd𝜔))
8718, 86bitrd 268 . 2 (𝑋 ∈ V → (𝑋 ≼ ω ↔ 𝒫 𝑋 ∈ 2nd𝜔))
882, 3, 87pm5.21nii 367 1 (𝑋 ≼ ω ↔ 𝒫 𝑋 ∈ 2nd𝜔)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383   = wceq 1596  wcel 2103  wral 3014  wrex 3015  Vcvv 3304  wss 3680  𝒫 cpw 4266  {csn 4285   class class class wbr 4760  cmpt 4837  ran crn 5219  wf 5997  1-1wf1 5998  1-1-ontowf1o 6000  cfv 6001  ωcom 7182  cen 8069  cdom 8070  topGenctg 16221  Topctop 20821  TopBasesctb 20872  2nd𝜔c2ndc 21364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-rep 4879  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-ral 3019  df-rex 3020  df-reu 3021  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-id 5128  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-er 7862  df-en 8073  df-dom 8074  df-topgen 16227  df-top 20822  df-bases 20873  df-2ndc 21366
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator