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

Theorem 2ndc1stc 21475
Description: A second-countable space is first-countable. (Contributed by Jeff Hankins, 17-Jan-2010.)
Assertion
Ref Expression
2ndc1stc (𝐽 ∈ 2nd𝜔 → 𝐽 ∈ 1st𝜔)

Proof of Theorem 2ndc1stc
Dummy variables 𝑜 𝑏 𝑝 𝑞 𝑠 𝑡 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2ndctop 21471 . 2 (𝐽 ∈ 2nd𝜔 → 𝐽 ∈ Top)
2 is2ndc 21470 . . . 4 (𝐽 ∈ 2nd𝜔 ↔ ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽))
3 ssrab2 3836 . . . . . . . . . . 11 {𝑞𝑏𝑥𝑞} ⊆ 𝑏
4 bastg 20991 . . . . . . . . . . . 12 (𝑏 ∈ TopBases → 𝑏 ⊆ (topGen‘𝑏))
543ad2ant1 1127 . . . . . . . . . . 11 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) → 𝑏 ⊆ (topGen‘𝑏))
63, 5syl5ss 3763 . . . . . . . . . 10 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) → {𝑞𝑏𝑥𝑞} ⊆ (topGen‘𝑏))
7 fvex 6342 . . . . . . . . . . 11 (topGen‘𝑏) ∈ V
87elpw2 4959 . . . . . . . . . 10 ({𝑞𝑏𝑥𝑞} ∈ 𝒫 (topGen‘𝑏) ↔ {𝑞𝑏𝑥𝑞} ⊆ (topGen‘𝑏))
96, 8sylibr 224 . . . . . . . . 9 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) → {𝑞𝑏𝑥𝑞} ∈ 𝒫 (topGen‘𝑏))
10 vex 3354 . . . . . . . . . . 11 𝑏 ∈ V
11 ssdomg 8155 . . . . . . . . . . 11 (𝑏 ∈ V → ({𝑞𝑏𝑥𝑞} ⊆ 𝑏 → {𝑞𝑏𝑥𝑞} ≼ 𝑏))
1210, 3, 11mp2 9 . . . . . . . . . 10 {𝑞𝑏𝑥𝑞} ≼ 𝑏
13 simp2 1131 . . . . . . . . . 10 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) → 𝑏 ≼ ω)
14 domtr 8162 . . . . . . . . . 10 (({𝑞𝑏𝑥𝑞} ≼ 𝑏𝑏 ≼ ω) → {𝑞𝑏𝑥𝑞} ≼ ω)
1512, 13, 14sylancr 567 . . . . . . . . 9 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) → {𝑞𝑏𝑥𝑞} ≼ ω)
16 eltg2b 20984 . . . . . . . . . . . 12 (𝑏 ∈ TopBases → (𝑜 ∈ (topGen‘𝑏) ↔ ∀𝑦𝑜𝑡𝑏 (𝑦𝑡𝑡𝑜)))
17163ad2ant1 1127 . . . . . . . . . . 11 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) → (𝑜 ∈ (topGen‘𝑏) ↔ ∀𝑦𝑜𝑡𝑏 (𝑦𝑡𝑡𝑜)))
18 elequ1 2152 . . . . . . . . . . . . . . 15 (𝑦 = 𝑥 → (𝑦𝑡𝑥𝑡))
1918anbi1d 607 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → ((𝑦𝑡𝑡𝑜) ↔ (𝑥𝑡𝑡𝑜)))
2019rexbidv 3200 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → (∃𝑡𝑏 (𝑦𝑡𝑡𝑜) ↔ ∃𝑡𝑏 (𝑥𝑡𝑡𝑜)))
2120rspccv 3457 . . . . . . . . . . . 12 (∀𝑦𝑜𝑡𝑏 (𝑦𝑡𝑡𝑜) → (𝑥𝑜 → ∃𝑡𝑏 (𝑥𝑡𝑡𝑜)))
22 id 22 . . . . . . . . . . . . . . . . 17 ((𝑡𝑏𝑥𝑡) → (𝑡𝑏𝑥𝑡))
2322adantrr 688 . . . . . . . . . . . . . . . 16 ((𝑡𝑏 ∧ (𝑥𝑡𝑡𝑜)) → (𝑡𝑏𝑥𝑡))
24 elequ2 2159 . . . . . . . . . . . . . . . . 17 (𝑞 = 𝑡 → (𝑥𝑞𝑥𝑡))
2524elrab 3515 . . . . . . . . . . . . . . . 16 (𝑡 ∈ {𝑞𝑏𝑥𝑞} ↔ (𝑡𝑏𝑥𝑡))
2623, 25sylibr 224 . . . . . . . . . . . . . . 15 ((𝑡𝑏 ∧ (𝑥𝑡𝑡𝑜)) → 𝑡 ∈ {𝑞𝑏𝑥𝑞})
2726adantl 467 . . . . . . . . . . . . . 14 (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) ∧ (𝑡𝑏 ∧ (𝑥𝑡𝑡𝑜))) → 𝑡 ∈ {𝑞𝑏𝑥𝑞})
28 simprr 748 . . . . . . . . . . . . . 14 (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) ∧ (𝑡𝑏 ∧ (𝑥𝑡𝑡𝑜))) → (𝑥𝑡𝑡𝑜))
29 elequ2 2159 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑡 → (𝑥𝑝𝑥𝑡))
30 sseq1 3775 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑡 → (𝑝𝑜𝑡𝑜))
3129, 30anbi12d 608 . . . . . . . . . . . . . . 15 (𝑝 = 𝑡 → ((𝑥𝑝𝑝𝑜) ↔ (𝑥𝑡𝑡𝑜)))
3231rspcev 3460 . . . . . . . . . . . . . 14 ((𝑡 ∈ {𝑞𝑏𝑥𝑞} ∧ (𝑥𝑡𝑡𝑜)) → ∃𝑝 ∈ {𝑞𝑏𝑥𝑞} (𝑥𝑝𝑝𝑜))
3327, 28, 32syl2anc 565 . . . . . . . . . . . . 13 (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) ∧ (𝑡𝑏 ∧ (𝑥𝑡𝑡𝑜))) → ∃𝑝 ∈ {𝑞𝑏𝑥𝑞} (𝑥𝑝𝑝𝑜))
3433rexlimdvaa 3180 . . . . . . . . . . . 12 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) → (∃𝑡𝑏 (𝑥𝑡𝑡𝑜) → ∃𝑝 ∈ {𝑞𝑏𝑥𝑞} (𝑥𝑝𝑝𝑜)))
3521, 34syl9r 78 . . . . . . . . . . 11 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) → (∀𝑦𝑜𝑡𝑏 (𝑦𝑡𝑡𝑜) → (𝑥𝑜 → ∃𝑝 ∈ {𝑞𝑏𝑥𝑞} (𝑥𝑝𝑝𝑜))))
3617, 35sylbid 230 . . . . . . . . . 10 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) → (𝑜 ∈ (topGen‘𝑏) → (𝑥𝑜 → ∃𝑝 ∈ {𝑞𝑏𝑥𝑞} (𝑥𝑝𝑝𝑜))))
3736ralrimiv 3114 . . . . . . . . 9 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) → ∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝 ∈ {𝑞𝑏𝑥𝑞} (𝑥𝑝𝑝𝑜)))
38 breq1 4789 . . . . . . . . . . 11 (𝑠 = {𝑞𝑏𝑥𝑞} → (𝑠 ≼ ω ↔ {𝑞𝑏𝑥𝑞} ≼ ω))
39 rexeq 3288 . . . . . . . . . . . . 13 (𝑠 = {𝑞𝑏𝑥𝑞} → (∃𝑝𝑠 (𝑥𝑝𝑝𝑜) ↔ ∃𝑝 ∈ {𝑞𝑏𝑥𝑞} (𝑥𝑝𝑝𝑜)))
4039imbi2d 329 . . . . . . . . . . . 12 (𝑠 = {𝑞𝑏𝑥𝑞} → ((𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜)) ↔ (𝑥𝑜 → ∃𝑝 ∈ {𝑞𝑏𝑥𝑞} (𝑥𝑝𝑝𝑜))))
4140ralbidv 3135 . . . . . . . . . . 11 (𝑠 = {𝑞𝑏𝑥𝑞} → (∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜)) ↔ ∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝 ∈ {𝑞𝑏𝑥𝑞} (𝑥𝑝𝑝𝑜))))
4238, 41anbi12d 608 . . . . . . . . . 10 (𝑠 = {𝑞𝑏𝑥𝑞} → ((𝑠 ≼ ω ∧ ∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜))) ↔ ({𝑞𝑏𝑥𝑞} ≼ ω ∧ ∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝 ∈ {𝑞𝑏𝑥𝑞} (𝑥𝑝𝑝𝑜)))))
4342rspcev 3460 . . . . . . . . 9 (({𝑞𝑏𝑥𝑞} ∈ 𝒫 (topGen‘𝑏) ∧ ({𝑞𝑏𝑥𝑞} ≼ ω ∧ ∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝 ∈ {𝑞𝑏𝑥𝑞} (𝑥𝑝𝑝𝑜)))) → ∃𝑠 ∈ 𝒫 (topGen‘𝑏)(𝑠 ≼ ω ∧ ∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜))))
449, 15, 37, 43syl12anc 1474 . . . . . . . 8 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) → ∃𝑠 ∈ 𝒫 (topGen‘𝑏)(𝑠 ≼ ω ∧ ∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜))))
45443expia 1114 . . . . . . 7 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) → (𝑥 (topGen‘𝑏) → ∃𝑠 ∈ 𝒫 (topGen‘𝑏)(𝑠 ≼ ω ∧ ∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜)))))
46 unieq 4582 . . . . . . . . 9 ((topGen‘𝑏) = 𝐽 (topGen‘𝑏) = 𝐽)
4746eleq2d 2836 . . . . . . . 8 ((topGen‘𝑏) = 𝐽 → (𝑥 (topGen‘𝑏) ↔ 𝑥 𝐽))
48 pweq 4300 . . . . . . . . 9 ((topGen‘𝑏) = 𝐽 → 𝒫 (topGen‘𝑏) = 𝒫 𝐽)
49 raleq 3287 . . . . . . . . . 10 ((topGen‘𝑏) = 𝐽 → (∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜)) ↔ ∀𝑜𝐽 (𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜))))
5049anbi2d 606 . . . . . . . . 9 ((topGen‘𝑏) = 𝐽 → ((𝑠 ≼ ω ∧ ∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜))) ↔ (𝑠 ≼ ω ∧ ∀𝑜𝐽 (𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜)))))
5148, 50rexeqbidv 3302 . . . . . . . 8 ((topGen‘𝑏) = 𝐽 → (∃𝑠 ∈ 𝒫 (topGen‘𝑏)(𝑠 ≼ ω ∧ ∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜))) ↔ ∃𝑠 ∈ 𝒫 𝐽(𝑠 ≼ ω ∧ ∀𝑜𝐽 (𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜)))))
5247, 51imbi12d 333 . . . . . . 7 ((topGen‘𝑏) = 𝐽 → ((𝑥 (topGen‘𝑏) → ∃𝑠 ∈ 𝒫 (topGen‘𝑏)(𝑠 ≼ ω ∧ ∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜)))) ↔ (𝑥 𝐽 → ∃𝑠 ∈ 𝒫 𝐽(𝑠 ≼ ω ∧ ∀𝑜𝐽 (𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜))))))
5345, 52syl5ibcom 235 . . . . . 6 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) → ((topGen‘𝑏) = 𝐽 → (𝑥 𝐽 → ∃𝑠 ∈ 𝒫 𝐽(𝑠 ≼ ω ∧ ∀𝑜𝐽 (𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜))))))
5453expimpd 441 . . . . 5 (𝑏 ∈ TopBases → ((𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽) → (𝑥 𝐽 → ∃𝑠 ∈ 𝒫 𝐽(𝑠 ≼ ω ∧ ∀𝑜𝐽 (𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜))))))
5554rexlimiv 3175 . . . 4 (∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽) → (𝑥 𝐽 → ∃𝑠 ∈ 𝒫 𝐽(𝑠 ≼ ω ∧ ∀𝑜𝐽 (𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜)))))
562, 55sylbi 207 . . 3 (𝐽 ∈ 2nd𝜔 → (𝑥 𝐽 → ∃𝑠 ∈ 𝒫 𝐽(𝑠 ≼ ω ∧ ∀𝑜𝐽 (𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜)))))
5756ralrimiv 3114 . 2 (𝐽 ∈ 2nd𝜔 → ∀𝑥 𝐽𝑠 ∈ 𝒫 𝐽(𝑠 ≼ ω ∧ ∀𝑜𝐽 (𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜))))
58 eqid 2771 . . 3 𝐽 = 𝐽
5958is1stc2 21466 . 2 (𝐽 ∈ 1st𝜔 ↔ (𝐽 ∈ Top ∧ ∀𝑥 𝐽𝑠 ∈ 𝒫 𝐽(𝑠 ≼ ω ∧ ∀𝑜𝐽 (𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜)))))
601, 57, 59sylanbrc 564 1 (𝐽 ∈ 2nd𝜔 → 𝐽 ∈ 1st𝜔)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wcel 2145  wral 3061  wrex 3062  {crab 3065  Vcvv 3351  wss 3723  𝒫 cpw 4297   cuni 4574   class class class wbr 4786  cfv 6031  ωcom 7212  cdom 8107  topGenctg 16306  Topctop 20918  TopBasesctb 20970  1st𝜔c1stc 21461  2nd𝜔c2ndc 21462
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-dom 8111  df-topgen 16312  df-top 20919  df-bases 20971  df-1stc 21463  df-2ndc 21464
This theorem is referenced by:  dis1stc  21523
  Copyright terms: Public domain W3C validator