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

Theorem dis2ndc 21589
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 8199 . . 3 Rel ≼
21brrelex1i 5361 . 2 (𝑋 ≼ ω → 𝑋 ∈ V)
3 pwexr 7205 . 2 (𝒫 𝑋 ∈ 2nd𝜔 → 𝑋 ∈ V)
4 elex 3398 . . . . 5 (𝑋 ∈ V → 𝑋 ∈ V)
5 snex 5097 . . . . . . . 8 {𝑥} ∈ V
652a1i 12 . . . . . . 7 (𝑋 ∈ V → (𝑥𝑋 → {𝑥} ∈ V))
7 vex 3386 . . . . . . . . . 10 𝑥 ∈ V
87sneqr 4555 . . . . . . . . 9 ({𝑥} = {𝑦} → 𝑥 = 𝑦)
9 sneq 4376 . . . . . . . . 9 (𝑥 = 𝑦 → {𝑥} = {𝑦})
108, 9impbii 201 . . . . . . . 8 ({𝑥} = {𝑦} ↔ 𝑥 = 𝑦)
11102a1i 12 . . . . . . 7 (𝑋 ∈ V → ((𝑥𝑋𝑦𝑋) → ({𝑥} = {𝑦} ↔ 𝑥 = 𝑦)))
126, 11dom2lem 8233 . . . . . 6 (𝑋 ∈ V → (𝑥𝑋 ↦ {𝑥}):𝑋1-1→V)
13 f1f1orn 6365 . . . . . 6 ((𝑥𝑋 ↦ {𝑥}):𝑋1-1→V → (𝑥𝑋 ↦ {𝑥}):𝑋1-1-onto→ran (𝑥𝑋 ↦ {𝑥}))
1412, 13syl 17 . . . . 5 (𝑋 ∈ V → (𝑥𝑋 ↦ {𝑥}):𝑋1-1-onto→ran (𝑥𝑋 ↦ {𝑥}))
15 f1oeng 8212 . . . . 5 ((𝑋 ∈ V ∧ (𝑥𝑋 ↦ {𝑥}):𝑋1-1-onto→ran (𝑥𝑋 ↦ {𝑥})) → 𝑋 ≈ ran (𝑥𝑋 ↦ {𝑥}))
164, 14, 15syl2anc 580 . . . 4 (𝑋 ∈ V → 𝑋 ≈ ran (𝑥𝑋 ↦ {𝑥}))
17 domen1 8342 . . . 4 (𝑋 ≈ ran (𝑥𝑋 ↦ {𝑥}) → (𝑋 ≼ ω ↔ ran (𝑥𝑋 ↦ {𝑥}) ≼ ω))
1816, 17syl 17 . . 3 (𝑋 ∈ V → (𝑋 ≼ ω ↔ ran (𝑥𝑋 ↦ {𝑥}) ≼ ω))
19 distop 21125 . . . . . . 7 (𝑋 ∈ V → 𝒫 𝑋 ∈ Top)
20 simpr 478 . . . . . . . . . 10 ((𝑋 ∈ V ∧ 𝑥𝑋) → 𝑥𝑋)
217snelpw 5102 . . . . . . . . . 10 (𝑥𝑋 ↔ {𝑥} ∈ 𝒫 𝑋)
2220, 21sylib 210 . . . . . . . . 9 ((𝑋 ∈ V ∧ 𝑥𝑋) → {𝑥} ∈ 𝒫 𝑋)
2322fmpttd 6609 . . . . . . . 8 (𝑋 ∈ V → (𝑥𝑋 ↦ {𝑥}):𝑋⟶𝒫 𝑋)
2423frnd 6261 . . . . . . 7 (𝑋 ∈ V → ran (𝑥𝑋 ↦ {𝑥}) ⊆ 𝒫 𝑋)
25 elpwi 4357 . . . . . . . . . . . . 13 (𝑦 ∈ 𝒫 𝑋𝑦𝑋)
2625ad2antrl 720 . . . . . . . . . . . 12 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → 𝑦𝑋)
27 simprr 790 . . . . . . . . . . . 12 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → 𝑧𝑦)
2826, 27sseldd 3797 . . . . . . . . . . 11 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → 𝑧𝑋)
29 eqidd 2798 . . . . . . . . . . 11 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → {𝑧} = {𝑧})
30 sneq 4376 . . . . . . . . . . . 12 (𝑥 = 𝑧 → {𝑥} = {𝑧})
3130rspceeqv 3513 . . . . . . . . . . 11 ((𝑧𝑋 ∧ {𝑧} = {𝑧}) → ∃𝑥𝑋 {𝑧} = {𝑥})
3228, 29, 31syl2anc 580 . . . . . . . . . 10 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → ∃𝑥𝑋 {𝑧} = {𝑥})
33 snex 5097 . . . . . . . . . . 11 {𝑧} ∈ V
34 eqid 2797 . . . . . . . . . . . 12 (𝑥𝑋 ↦ {𝑥}) = (𝑥𝑋 ↦ {𝑥})
3534elrnmpt 5574 . . . . . . . . . . 11 ({𝑧} ∈ V → ({𝑧} ∈ ran (𝑥𝑋 ↦ {𝑥}) ↔ ∃𝑥𝑋 {𝑧} = {𝑥}))
3633, 35ax-mp 5 . . . . . . . . . 10 ({𝑧} ∈ ran (𝑥𝑋 ↦ {𝑥}) ↔ ∃𝑥𝑋 {𝑧} = {𝑥})
3732, 36sylibr 226 . . . . . . . . 9 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → {𝑧} ∈ ran (𝑥𝑋 ↦ {𝑥}))
38 vsnid 4399 . . . . . . . . . 10 𝑧 ∈ {𝑧}
3938a1i 11 . . . . . . . . 9 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → 𝑧 ∈ {𝑧})
4027snssd 4526 . . . . . . . . 9 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → {𝑧} ⊆ 𝑦)
41 eleq2 2865 . . . . . . . . . . 11 (𝑤 = {𝑧} → (𝑧𝑤𝑧 ∈ {𝑧}))
42 sseq1 3820 . . . . . . . . . . 11 (𝑤 = {𝑧} → (𝑤𝑦 ↔ {𝑧} ⊆ 𝑦))
4341, 42anbi12d 625 . . . . . . . . . 10 (𝑤 = {𝑧} → ((𝑧𝑤𝑤𝑦) ↔ (𝑧 ∈ {𝑧} ∧ {𝑧} ⊆ 𝑦)))
4443rspcev 3495 . . . . . . . . 9 (({𝑧} ∈ ran (𝑥𝑋 ↦ {𝑥}) ∧ (𝑧 ∈ {𝑧} ∧ {𝑧} ⊆ 𝑦)) → ∃𝑤 ∈ ran (𝑥𝑋 ↦ {𝑥})(𝑧𝑤𝑤𝑦))
4537, 39, 40, 44syl12anc 866 . . . . . . . 8 ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋𝑧𝑦)) → ∃𝑤 ∈ ran (𝑥𝑋 ↦ {𝑥})(𝑧𝑤𝑤𝑦))
4645ralrimivva 3150 . . . . . . 7 (𝑋 ∈ V → ∀𝑦 ∈ 𝒫 𝑋𝑧𝑦𝑤 ∈ ran (𝑥𝑋 ↦ {𝑥})(𝑧𝑤𝑤𝑦))
47 basgen2 21119 . . . . . . 7 ((𝒫 𝑋 ∈ Top ∧ ran (𝑥𝑋 ↦ {𝑥}) ⊆ 𝒫 𝑋 ∧ ∀𝑦 ∈ 𝒫 𝑋𝑧𝑦𝑤 ∈ ran (𝑥𝑋 ↦ {𝑥})(𝑧𝑤𝑤𝑦)) → (topGen‘ran (𝑥𝑋 ↦ {𝑥})) = 𝒫 𝑋)
4819, 24, 46, 47syl3anc 1491 . . . . . 6 (𝑋 ∈ V → (topGen‘ran (𝑥𝑋 ↦ {𝑥})) = 𝒫 𝑋)
4948adantr 473 . . . . 5 ((𝑋 ∈ V ∧ ran (𝑥𝑋 ↦ {𝑥}) ≼ ω) → (topGen‘ran (𝑥𝑋 ↦ {𝑥})) = 𝒫 𝑋)
5048, 19eqeltrd 2876 . . . . . . 7 (𝑋 ∈ V → (topGen‘ran (𝑥𝑋 ↦ {𝑥})) ∈ Top)
51 tgclb 21100 . . . . . . 7 (ran (𝑥𝑋 ↦ {𝑥}) ∈ TopBases ↔ (topGen‘ran (𝑥𝑋 ↦ {𝑥})) ∈ Top)
5250, 51sylibr 226 . . . . . 6 (𝑋 ∈ V → ran (𝑥𝑋 ↦ {𝑥}) ∈ TopBases)
53 2ndci 21577 . . . . . 6 ((ran (𝑥𝑋 ↦ {𝑥}) ∈ TopBases ∧ ran (𝑥𝑋 ↦ {𝑥}) ≼ ω) → (topGen‘ran (𝑥𝑋 ↦ {𝑥})) ∈ 2nd𝜔)
5452, 53sylan 576 . . . . 5 ((𝑋 ∈ V ∧ ran (𝑥𝑋 ↦ {𝑥}) ≼ ω) → (topGen‘ran (𝑥𝑋 ↦ {𝑥})) ∈ 2nd𝜔)
5549, 54eqeltrrd 2877 . . . 4 ((𝑋 ∈ V ∧ ran (𝑥𝑋 ↦ {𝑥}) ≼ ω) → 𝒫 𝑋 ∈ 2nd𝜔)
56 is2ndc 21575 . . . . . 6 (𝒫 𝑋 ∈ 2nd𝜔 ↔ ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋))
57 vex 3386 . . . . . . . . . 10 𝑏 ∈ V
58 simpr 478 . . . . . . . . . . . . . . . 16 ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) → 𝑥𝑋)
5958, 21sylib 210 . . . . . . . . . . . . . . 15 ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) → {𝑥} ∈ 𝒫 𝑋)
60 simplrr 797 . . . . . . . . . . . . . . 15 ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) → (topGen‘𝑏) = 𝒫 𝑋)
6159, 60eleqtrrd 2879 . . . . . . . . . . . . . 14 ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) → {𝑥} ∈ (topGen‘𝑏))
62 vsnid 4399 . . . . . . . . . . . . . 14 𝑥 ∈ {𝑥}
63 tg2 21095 . . . . . . . . . . . . . 14 (({𝑥} ∈ (topGen‘𝑏) ∧ 𝑥 ∈ {𝑥}) → ∃𝑦𝑏 (𝑥𝑦𝑦 ⊆ {𝑥}))
6461, 62, 63sylancl 581 . . . . . . . . . . . . 13 ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) → ∃𝑦𝑏 (𝑥𝑦𝑦 ⊆ {𝑥}))
65 simprrl 800 . . . . . . . . . . . . . . . 16 (((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) ∧ (𝑦𝑏 ∧ (𝑥𝑦𝑦 ⊆ {𝑥}))) → 𝑥𝑦)
6665snssd 4526 . . . . . . . . . . . . . . 15 (((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) ∧ (𝑦𝑏 ∧ (𝑥𝑦𝑦 ⊆ {𝑥}))) → {𝑥} ⊆ 𝑦)
67 simprrr 801 . . . . . . . . . . . . . . 15 (((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) ∧ (𝑦𝑏 ∧ (𝑥𝑦𝑦 ⊆ {𝑥}))) → 𝑦 ⊆ {𝑥})
6866, 67eqssd 3813 . . . . . . . . . . . . . 14 (((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) ∧ (𝑦𝑏 ∧ (𝑥𝑦𝑦 ⊆ {𝑥}))) → {𝑥} = 𝑦)
69 simprl 788 . . . . . . . . . . . . . 14 (((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) ∧ (𝑦𝑏 ∧ (𝑥𝑦𝑦 ⊆ {𝑥}))) → 𝑦𝑏)
7068, 69eqeltrd 2876 . . . . . . . . . . . . 13 (((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) ∧ (𝑦𝑏 ∧ (𝑥𝑦𝑦 ⊆ {𝑥}))) → {𝑥} ∈ 𝑏)
7164, 70rexlimddv 3214 . . . . . . . . . . . 12 ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) ∧ 𝑥𝑋) → {𝑥} ∈ 𝑏)
7271fmpttd 6609 . . . . . . . . . . 11 (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) → (𝑥𝑋 ↦ {𝑥}):𝑋𝑏)
7372frnd 6261 . . . . . . . . . 10 (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) → ran (𝑥𝑋 ↦ {𝑥}) ⊆ 𝑏)
74 ssdomg 8239 . . . . . . . . . 10 (𝑏 ∈ V → (ran (𝑥𝑋 ↦ {𝑥}) ⊆ 𝑏 → ran (𝑥𝑋 ↦ {𝑥}) ≼ 𝑏))
7557, 73, 74mpsyl 68 . . . . . . . . 9 (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) → ran (𝑥𝑋 ↦ {𝑥}) ≼ 𝑏)
76 simprl 788 . . . . . . . . 9 (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) → 𝑏 ≼ ω)
77 domtr 8246 . . . . . . . . 9 ((ran (𝑥𝑋 ↦ {𝑥}) ≼ 𝑏𝑏 ≼ ω) → ran (𝑥𝑋 ↦ {𝑥}) ≼ ω)
7875, 76, 77syl2anc 580 . . . . . . . 8 (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) → ran (𝑥𝑋 ↦ {𝑥}) ≼ ω)
7978ex 402 . . . . . . 7 ((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) → ((𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋) → ran (𝑥𝑋 ↦ {𝑥}) ≼ ω))
8079rexlimdva 3210 . . . . . 6 (𝑋 ∈ V → (∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋) → ran (𝑥𝑋 ↦ {𝑥}) ≼ ω))
8156, 80syl5bi 234 . . . . 5 (𝑋 ∈ V → (𝒫 𝑋 ∈ 2nd𝜔 → ran (𝑥𝑋 ↦ {𝑥}) ≼ ω))
8281imp 396 . . . 4 ((𝑋 ∈ V ∧ 𝒫 𝑋 ∈ 2nd𝜔) → ran (𝑥𝑋 ↦ {𝑥}) ≼ ω)
8355, 82impbida 836 . . 3 (𝑋 ∈ V → (ran (𝑥𝑋 ↦ {𝑥}) ≼ ω ↔ 𝒫 𝑋 ∈ 2nd𝜔))
8418, 83bitrd 271 . 2 (𝑋 ∈ V → (𝑋 ≼ ω ↔ 𝒫 𝑋 ∈ 2nd𝜔))
852, 3, 84pm5.21nii 370 1 (𝑋 ≼ ω ↔ 𝒫 𝑋 ∈ 2nd𝜔)
Colors of variables: wff setvar class
Syntax hints:  wb 198  wa 385   = wceq 1653  wcel 2157  wral 3087  wrex 3088  Vcvv 3383  wss 3767  𝒫 cpw 4347  {csn 4366   class class class wbr 4841  cmpt 4920  ran crn 5311  1-1wf1 6096  1-1-ontowf1o 6098  cfv 6099  ωcom 7297  cen 8190  cdom 8191  topGenctg 16410  Topctop 21023  TopBasesctb 21075  2nd𝜔c2ndc 21567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2354  ax-ext 2775  ax-rep 4962  ax-sep 4973  ax-nul 4981  ax-pow 5033  ax-pr 5095  ax-un 7181
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2590  df-eu 2607  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-ne 2970  df-ral 3092  df-rex 3093  df-reu 3094  df-rab 3096  df-v 3385  df-sbc 3632  df-csb 3727  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4114  df-if 4276  df-pw 4349  df-sn 4367  df-pr 4369  df-op 4373  df-uni 4627  df-iun 4710  df-br 4842  df-opab 4904  df-mpt 4921  df-id 5218  df-xp 5316  df-rel 5317  df-cnv 5318  df-co 5319  df-dm 5320  df-rn 5321  df-res 5322  df-ima 5323  df-iota 6062  df-fun 6101  df-fn 6102  df-f 6103  df-f1 6104  df-fo 6105  df-f1o 6106  df-fv 6107  df-er 7980  df-en 8194  df-dom 8195  df-topgen 16416  df-top 21024  df-bases 21076  df-2ndc 21569
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator