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

Theorem 2ndc1stc 21302
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 21298 . 2 (𝐽 ∈ 2nd𝜔 → 𝐽 ∈ Top)
2 is2ndc 21297 . . . 4 (𝐽 ∈ 2nd𝜔 ↔ ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽))
3 ssrab2 3720 . . . . . . . . . . 11 {𝑞𝑏𝑥𝑞} ⊆ 𝑏
4 bastg 20818 . . . . . . . . . . . 12 (𝑏 ∈ TopBases → 𝑏 ⊆ (topGen‘𝑏))
543ad2ant1 1102 . . . . . . . . . . 11 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) → 𝑏 ⊆ (topGen‘𝑏))
63, 5syl5ss 3647 . . . . . . . . . 10 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) → {𝑞𝑏𝑥𝑞} ⊆ (topGen‘𝑏))
7 fvex 6239 . . . . . . . . . . 11 (topGen‘𝑏) ∈ V
87elpw2 4858 . . . . . . . . . 10 ({𝑞𝑏𝑥𝑞} ∈ 𝒫 (topGen‘𝑏) ↔ {𝑞𝑏𝑥𝑞} ⊆ (topGen‘𝑏))
96, 8sylibr 224 . . . . . . . . 9 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) → {𝑞𝑏𝑥𝑞} ∈ 𝒫 (topGen‘𝑏))
10 vex 3234 . . . . . . . . . . 11 𝑏 ∈ V
11 ssdomg 8043 . . . . . . . . . . 11 (𝑏 ∈ V → ({𝑞𝑏𝑥𝑞} ⊆ 𝑏 → {𝑞𝑏𝑥𝑞} ≼ 𝑏))
1210, 3, 11mp2 9 . . . . . . . . . 10 {𝑞𝑏𝑥𝑞} ≼ 𝑏
13 simp2 1082 . . . . . . . . . 10 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) → 𝑏 ≼ ω)
14 domtr 8050 . . . . . . . . . 10 (({𝑞𝑏𝑥𝑞} ≼ 𝑏𝑏 ≼ ω) → {𝑞𝑏𝑥𝑞} ≼ ω)
1512, 13, 14sylancr 696 . . . . . . . . 9 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) → {𝑞𝑏𝑥𝑞} ≼ ω)
16 eltg2b 20811 . . . . . . . . . . . 12 (𝑏 ∈ TopBases → (𝑜 ∈ (topGen‘𝑏) ↔ ∀𝑦𝑜𝑡𝑏 (𝑦𝑡𝑡𝑜)))
17163ad2ant1 1102 . . . . . . . . . . 11 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) → (𝑜 ∈ (topGen‘𝑏) ↔ ∀𝑦𝑜𝑡𝑏 (𝑦𝑡𝑡𝑜)))
18 elequ1 2037 . . . . . . . . . . . . . . 15 (𝑦 = 𝑥 → (𝑦𝑡𝑥𝑡))
1918anbi1d 741 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → ((𝑦𝑡𝑡𝑜) ↔ (𝑥𝑡𝑡𝑜)))
2019rexbidv 3081 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → (∃𝑡𝑏 (𝑦𝑡𝑡𝑜) ↔ ∃𝑡𝑏 (𝑥𝑡𝑡𝑜)))
2120rspccv 3337 . . . . . . . . . . . 12 (∀𝑦𝑜𝑡𝑏 (𝑦𝑡𝑡𝑜) → (𝑥𝑜 → ∃𝑡𝑏 (𝑥𝑡𝑡𝑜)))
22 id 22 . . . . . . . . . . . . . . . . 17 ((𝑡𝑏𝑥𝑡) → (𝑡𝑏𝑥𝑡))
2322adantrr 753 . . . . . . . . . . . . . . . 16 ((𝑡𝑏 ∧ (𝑥𝑡𝑡𝑜)) → (𝑡𝑏𝑥𝑡))
24 elequ2 2044 . . . . . . . . . . . . . . . . 17 (𝑞 = 𝑡 → (𝑥𝑞𝑥𝑡))
2524elrab 3396 . . . . . . . . . . . . . . . 16 (𝑡 ∈ {𝑞𝑏𝑥𝑞} ↔ (𝑡𝑏𝑥𝑡))
2623, 25sylibr 224 . . . . . . . . . . . . . . 15 ((𝑡𝑏 ∧ (𝑥𝑡𝑡𝑜)) → 𝑡 ∈ {𝑞𝑏𝑥𝑞})
2726adantl 481 . . . . . . . . . . . . . 14 (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) ∧ (𝑡𝑏 ∧ (𝑥𝑡𝑡𝑜))) → 𝑡 ∈ {𝑞𝑏𝑥𝑞})
28 simprr 811 . . . . . . . . . . . . . 14 (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) ∧ (𝑡𝑏 ∧ (𝑥𝑡𝑡𝑜))) → (𝑥𝑡𝑡𝑜))
29 elequ2 2044 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑡 → (𝑥𝑝𝑥𝑡))
30 sseq1 3659 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑡 → (𝑝𝑜𝑡𝑜))
3129, 30anbi12d 747 . . . . . . . . . . . . . . 15 (𝑝 = 𝑡 → ((𝑥𝑝𝑝𝑜) ↔ (𝑥𝑡𝑡𝑜)))
3231rspcev 3340 . . . . . . . . . . . . . 14 ((𝑡 ∈ {𝑞𝑏𝑥𝑞} ∧ (𝑥𝑡𝑡𝑜)) → ∃𝑝 ∈ {𝑞𝑏𝑥𝑞} (𝑥𝑝𝑝𝑜))
3327, 28, 32syl2anc 694 . . . . . . . . . . . . 13 (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) ∧ (𝑡𝑏 ∧ (𝑥𝑡𝑡𝑜))) → ∃𝑝 ∈ {𝑞𝑏𝑥𝑞} (𝑥𝑝𝑝𝑜))
3433rexlimdvaa 3061 . . . . . . . . . . . 12 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) → (∃𝑡𝑏 (𝑥𝑡𝑡𝑜) → ∃𝑝 ∈ {𝑞𝑏𝑥𝑞} (𝑥𝑝𝑝𝑜)))
3521, 34syl9r 78 . . . . . . . . . . 11 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) → (∀𝑦𝑜𝑡𝑏 (𝑦𝑡𝑡𝑜) → (𝑥𝑜 → ∃𝑝 ∈ {𝑞𝑏𝑥𝑞} (𝑥𝑝𝑝𝑜))))
3617, 35sylbid 230 . . . . . . . . . 10 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) → (𝑜 ∈ (topGen‘𝑏) → (𝑥𝑜 → ∃𝑝 ∈ {𝑞𝑏𝑥𝑞} (𝑥𝑝𝑝𝑜))))
3736ralrimiv 2994 . . . . . . . . 9 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) → ∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝 ∈ {𝑞𝑏𝑥𝑞} (𝑥𝑝𝑝𝑜)))
38 breq1 4688 . . . . . . . . . . 11 (𝑠 = {𝑞𝑏𝑥𝑞} → (𝑠 ≼ ω ↔ {𝑞𝑏𝑥𝑞} ≼ ω))
39 rexeq 3169 . . . . . . . . . . . . 13 (𝑠 = {𝑞𝑏𝑥𝑞} → (∃𝑝𝑠 (𝑥𝑝𝑝𝑜) ↔ ∃𝑝 ∈ {𝑞𝑏𝑥𝑞} (𝑥𝑝𝑝𝑜)))
4039imbi2d 329 . . . . . . . . . . . 12 (𝑠 = {𝑞𝑏𝑥𝑞} → ((𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜)) ↔ (𝑥𝑜 → ∃𝑝 ∈ {𝑞𝑏𝑥𝑞} (𝑥𝑝𝑝𝑜))))
4140ralbidv 3015 . . . . . . . . . . 11 (𝑠 = {𝑞𝑏𝑥𝑞} → (∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜)) ↔ ∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝 ∈ {𝑞𝑏𝑥𝑞} (𝑥𝑝𝑝𝑜))))
4238, 41anbi12d 747 . . . . . . . . . 10 (𝑠 = {𝑞𝑏𝑥𝑞} → ((𝑠 ≼ ω ∧ ∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜))) ↔ ({𝑞𝑏𝑥𝑞} ≼ ω ∧ ∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝 ∈ {𝑞𝑏𝑥𝑞} (𝑥𝑝𝑝𝑜)))))
4342rspcev 3340 . . . . . . . . 9 (({𝑞𝑏𝑥𝑞} ∈ 𝒫 (topGen‘𝑏) ∧ ({𝑞𝑏𝑥𝑞} ≼ ω ∧ ∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝 ∈ {𝑞𝑏𝑥𝑞} (𝑥𝑝𝑝𝑜)))) → ∃𝑠 ∈ 𝒫 (topGen‘𝑏)(𝑠 ≼ ω ∧ ∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜))))
449, 15, 37, 43syl12anc 1364 . . . . . . . 8 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 (topGen‘𝑏)) → ∃𝑠 ∈ 𝒫 (topGen‘𝑏)(𝑠 ≼ ω ∧ ∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜))))
45443expia 1286 . . . . . . 7 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) → (𝑥 (topGen‘𝑏) → ∃𝑠 ∈ 𝒫 (topGen‘𝑏)(𝑠 ≼ ω ∧ ∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜)))))
46 unieq 4476 . . . . . . . . 9 ((topGen‘𝑏) = 𝐽 (topGen‘𝑏) = 𝐽)
4746eleq2d 2716 . . . . . . . 8 ((topGen‘𝑏) = 𝐽 → (𝑥 (topGen‘𝑏) ↔ 𝑥 𝐽))
48 pweq 4194 . . . . . . . . 9 ((topGen‘𝑏) = 𝐽 → 𝒫 (topGen‘𝑏) = 𝒫 𝐽)
49 raleq 3168 . . . . . . . . . 10 ((topGen‘𝑏) = 𝐽 → (∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜)) ↔ ∀𝑜𝐽 (𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜))))
5049anbi2d 740 . . . . . . . . 9 ((topGen‘𝑏) = 𝐽 → ((𝑠 ≼ ω ∧ ∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜))) ↔ (𝑠 ≼ ω ∧ ∀𝑜𝐽 (𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜)))))
5148, 50rexeqbidv 3183 . . . . . . . 8 ((topGen‘𝑏) = 𝐽 → (∃𝑠 ∈ 𝒫 (topGen‘𝑏)(𝑠 ≼ ω ∧ ∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜))) ↔ ∃𝑠 ∈ 𝒫 𝐽(𝑠 ≼ ω ∧ ∀𝑜𝐽 (𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜)))))
5247, 51imbi12d 333 . . . . . . 7 ((topGen‘𝑏) = 𝐽 → ((𝑥 (topGen‘𝑏) → ∃𝑠 ∈ 𝒫 (topGen‘𝑏)(𝑠 ≼ ω ∧ ∀𝑜 ∈ (topGen‘𝑏)(𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜)))) ↔ (𝑥 𝐽 → ∃𝑠 ∈ 𝒫 𝐽(𝑠 ≼ ω ∧ ∀𝑜𝐽 (𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜))))))
5345, 52syl5ibcom 235 . . . . . 6 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) → ((topGen‘𝑏) = 𝐽 → (𝑥 𝐽 → ∃𝑠 ∈ 𝒫 𝐽(𝑠 ≼ ω ∧ ∀𝑜𝐽 (𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜))))))
5453expimpd 628 . . . . 5 (𝑏 ∈ TopBases → ((𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽) → (𝑥 𝐽 → ∃𝑠 ∈ 𝒫 𝐽(𝑠 ≼ ω ∧ ∀𝑜𝐽 (𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜))))))
5554rexlimiv 3056 . . . 4 (∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽) → (𝑥 𝐽 → ∃𝑠 ∈ 𝒫 𝐽(𝑠 ≼ ω ∧ ∀𝑜𝐽 (𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜)))))
562, 55sylbi 207 . . 3 (𝐽 ∈ 2nd𝜔 → (𝑥 𝐽 → ∃𝑠 ∈ 𝒫 𝐽(𝑠 ≼ ω ∧ ∀𝑜𝐽 (𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜)))))
5756ralrimiv 2994 . 2 (𝐽 ∈ 2nd𝜔 → ∀𝑥 𝐽𝑠 ∈ 𝒫 𝐽(𝑠 ≼ ω ∧ ∀𝑜𝐽 (𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜))))
58 eqid 2651 . . 3 𝐽 = 𝐽
5958is1stc2 21293 . 2 (𝐽 ∈ 1st𝜔 ↔ (𝐽 ∈ Top ∧ ∀𝑥 𝐽𝑠 ∈ 𝒫 𝐽(𝑠 ≼ ω ∧ ∀𝑜𝐽 (𝑥𝑜 → ∃𝑝𝑠 (𝑥𝑝𝑝𝑜)))))
601, 57, 59sylanbrc 699 1 (𝐽 ∈ 2nd𝜔 → 𝐽 ∈ 1st𝜔)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wral 2941  wrex 2942  {crab 2945  Vcvv 3231  wss 3607  𝒫 cpw 4191   cuni 4468   class class class wbr 4685  cfv 5926  ωcom 7107  cdom 7995  topGenctg 16145  Topctop 20746  TopBasesctb 20797  1st𝜔c1stc 21288  2nd𝜔c2ndc 21289
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-dom 7999  df-topgen 16151  df-top 20747  df-bases 20798  df-1stc 21290  df-2ndc 21291
This theorem is referenced by:  dis1stc  21350
  Copyright terms: Public domain W3C validator