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

Theorem 2ndcsep 22062
 Description: A second-countable topology is separable, which is to say it contains a countable dense subset. (Contributed by Mario Carneiro, 13-Apr-2015.)
Hypothesis
Ref Expression
2ndcsep.1 𝑋 = 𝐽
Assertion
Ref Expression
2ndcsep (𝐽 ∈ 2ndω → ∃𝑥 ∈ 𝒫 𝑋(𝑥 ≼ ω ∧ ((cls‘𝐽)‘𝑥) = 𝑋))
Distinct variable groups:   𝑥,𝐽   𝑥,𝑋

Proof of Theorem 2ndcsep
Dummy variables 𝑓 𝑏 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 is2ndc 22049 . 2 (𝐽 ∈ 2ndω ↔ ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽))
2 vex 3483 . . . . . . . . 9 𝑏 ∈ V
3 difss 4094 . . . . . . . . 9 (𝑏 ∖ {∅}) ⊆ 𝑏
4 ssdomg 8547 . . . . . . . . 9 (𝑏 ∈ V → ((𝑏 ∖ {∅}) ⊆ 𝑏 → (𝑏 ∖ {∅}) ≼ 𝑏))
52, 3, 4mp2 9 . . . . . . . 8 (𝑏 ∖ {∅}) ≼ 𝑏
6 simpr 488 . . . . . . . 8 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) → 𝑏 ≼ ω)
7 domtr 8554 . . . . . . . 8 (((𝑏 ∖ {∅}) ≼ 𝑏𝑏 ≼ ω) → (𝑏 ∖ {∅}) ≼ ω)
85, 6, 7sylancr 590 . . . . . . 7 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) → (𝑏 ∖ {∅}) ≼ ω)
9 eldifsn 4704 . . . . . . . . 9 (𝑦 ∈ (𝑏 ∖ {∅}) ↔ (𝑦𝑏𝑦 ≠ ∅))
10 n0 4293 . . . . . . . . . 10 (𝑦 ≠ ∅ ↔ ∃𝑧 𝑧𝑦)
11 elunii 4830 . . . . . . . . . . . . . . 15 ((𝑧𝑦𝑦𝑏) → 𝑧 𝑏)
12 simpl 486 . . . . . . . . . . . . . . 15 ((𝑧𝑦𝑦𝑏) → 𝑧𝑦)
1311, 12jca 515 . . . . . . . . . . . . . 14 ((𝑧𝑦𝑦𝑏) → (𝑧 𝑏𝑧𝑦))
1413expcom 417 . . . . . . . . . . . . 13 (𝑦𝑏 → (𝑧𝑦 → (𝑧 𝑏𝑧𝑦)))
1514eximdv 1919 . . . . . . . . . . . 12 (𝑦𝑏 → (∃𝑧 𝑧𝑦 → ∃𝑧(𝑧 𝑏𝑧𝑦)))
1615imp 410 . . . . . . . . . . 11 ((𝑦𝑏 ∧ ∃𝑧 𝑧𝑦) → ∃𝑧(𝑧 𝑏𝑧𝑦))
17 df-rex 3139 . . . . . . . . . . 11 (∃𝑧 𝑏𝑧𝑦 ↔ ∃𝑧(𝑧 𝑏𝑧𝑦))
1816, 17sylibr 237 . . . . . . . . . 10 ((𝑦𝑏 ∧ ∃𝑧 𝑧𝑦) → ∃𝑧 𝑏𝑧𝑦)
1910, 18sylan2b 596 . . . . . . . . 9 ((𝑦𝑏𝑦 ≠ ∅) → ∃𝑧 𝑏𝑧𝑦)
209, 19sylbi 220 . . . . . . . 8 (𝑦 ∈ (𝑏 ∖ {∅}) → ∃𝑧 𝑏𝑧𝑦)
2120rgen 3143 . . . . . . 7 𝑦 ∈ (𝑏 ∖ {∅})∃𝑧 𝑏𝑧𝑦
22 vuniex 7456 . . . . . . . 8 𝑏 ∈ V
23 eleq1 2903 . . . . . . . 8 (𝑧 = (𝑓𝑦) → (𝑧𝑦 ↔ (𝑓𝑦) ∈ 𝑦))
2422, 23axcc4dom 9857 . . . . . . 7 (((𝑏 ∖ {∅}) ≼ ω ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})∃𝑧 𝑏𝑧𝑦) → ∃𝑓(𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦))
258, 21, 24sylancl 589 . . . . . 6 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) → ∃𝑓(𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦))
26 frn 6509 . . . . . . . . 9 (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 → ran 𝑓 𝑏)
2726ad2antrl 727 . . . . . . . 8 (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦)) → ran 𝑓 𝑏)
28 vex 3483 . . . . . . . . . 10 𝑓 ∈ V
2928rnex 7609 . . . . . . . . 9 ran 𝑓 ∈ V
3029elpw 4526 . . . . . . . 8 (ran 𝑓 ∈ 𝒫 𝑏 ↔ ran 𝑓 𝑏)
3127, 30sylibr 237 . . . . . . 7 (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦)) → ran 𝑓 ∈ 𝒫 𝑏)
32 omelon 9102 . . . . . . . . . . 11 ω ∈ On
336adantr 484 . . . . . . . . . . 11 (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦)) → 𝑏 ≼ ω)
34 ondomen 9457 . . . . . . . . . . 11 ((ω ∈ On ∧ 𝑏 ≼ ω) → 𝑏 ∈ dom card)
3532, 33, 34sylancr 590 . . . . . . . . . 10 (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦)) → 𝑏 ∈ dom card)
36 ssnum 9459 . . . . . . . . . 10 ((𝑏 ∈ dom card ∧ (𝑏 ∖ {∅}) ⊆ 𝑏) → (𝑏 ∖ {∅}) ∈ dom card)
3735, 3, 36sylancl 589 . . . . . . . . 9 (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦)) → (𝑏 ∖ {∅}) ∈ dom card)
38 ffn 6503 . . . . . . . . . . 11 (𝑓:(𝑏 ∖ {∅})⟶ 𝑏𝑓 Fn (𝑏 ∖ {∅}))
3938ad2antrl 727 . . . . . . . . . 10 (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦)) → 𝑓 Fn (𝑏 ∖ {∅}))
40 dffn4 6585 . . . . . . . . . 10 (𝑓 Fn (𝑏 ∖ {∅}) ↔ 𝑓:(𝑏 ∖ {∅})–onto→ran 𝑓)
4139, 40sylib 221 . . . . . . . . 9 (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦)) → 𝑓:(𝑏 ∖ {∅})–onto→ran 𝑓)
42 fodomnum 9477 . . . . . . . . 9 ((𝑏 ∖ {∅}) ∈ dom card → (𝑓:(𝑏 ∖ {∅})–onto→ran 𝑓 → ran 𝑓 ≼ (𝑏 ∖ {∅})))
4337, 41, 42sylc 65 . . . . . . . 8 (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦)) → ran 𝑓 ≼ (𝑏 ∖ {∅}))
448adantr 484 . . . . . . . 8 (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦)) → (𝑏 ∖ {∅}) ≼ ω)
45 domtr 8554 . . . . . . . 8 ((ran 𝑓 ≼ (𝑏 ∖ {∅}) ∧ (𝑏 ∖ {∅}) ≼ ω) → ran 𝑓 ≼ ω)
4643, 44, 45syl2anc 587 . . . . . . 7 (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦)) → ran 𝑓 ≼ ω)
47 tgcl 21572 . . . . . . . . . 10 (𝑏 ∈ TopBases → (topGen‘𝑏) ∈ Top)
4847ad2antrr 725 . . . . . . . . 9 (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦)) → (topGen‘𝑏) ∈ Top)
49 unitg 21570 . . . . . . . . . . . 12 (𝑏 ∈ V → (topGen‘𝑏) = 𝑏)
5049elv 3485 . . . . . . . . . . 11 (topGen‘𝑏) = 𝑏
5150eqcomi 2833 . . . . . . . . . 10 𝑏 = (topGen‘𝑏)
5251clsss3 21662 . . . . . . . . 9 (((topGen‘𝑏) ∈ Top ∧ ran 𝑓 𝑏) → ((cls‘(topGen‘𝑏))‘ran 𝑓) ⊆ 𝑏)
5348, 27, 52syl2anc 587 . . . . . . . 8 (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦)) → ((cls‘(topGen‘𝑏))‘ran 𝑓) ⊆ 𝑏)
54 ne0i 4283 . . . . . . . . . . . . . . . 16 (𝑥𝑦𝑦 ≠ ∅)
5554anim2i 619 . . . . . . . . . . . . . . 15 ((𝑦𝑏𝑥𝑦) → (𝑦𝑏𝑦 ≠ ∅))
5655, 9sylibr 237 . . . . . . . . . . . . . 14 ((𝑦𝑏𝑥𝑦) → 𝑦 ∈ (𝑏 ∖ {∅}))
57 fnfvelrn 6837 . . . . . . . . . . . . . . . . . 18 ((𝑓 Fn (𝑏 ∖ {∅}) ∧ 𝑦 ∈ (𝑏 ∖ {∅})) → (𝑓𝑦) ∈ ran 𝑓)
5838, 57sylan 583 . . . . . . . . . . . . . . . . 17 ((𝑓:(𝑏 ∖ {∅})⟶ 𝑏𝑦 ∈ (𝑏 ∖ {∅})) → (𝑓𝑦) ∈ ran 𝑓)
59 inelcm 4397 . . . . . . . . . . . . . . . . . 18 (((𝑓𝑦) ∈ 𝑦 ∧ (𝑓𝑦) ∈ ran 𝑓) → (𝑦 ∩ ran 𝑓) ≠ ∅)
6059expcom 417 . . . . . . . . . . . . . . . . 17 ((𝑓𝑦) ∈ ran 𝑓 → ((𝑓𝑦) ∈ 𝑦 → (𝑦 ∩ ran 𝑓) ≠ ∅))
6158, 60syl 17 . . . . . . . . . . . . . . . 16 ((𝑓:(𝑏 ∖ {∅})⟶ 𝑏𝑦 ∈ (𝑏 ∖ {∅})) → ((𝑓𝑦) ∈ 𝑦 → (𝑦 ∩ ran 𝑓) ≠ ∅))
6261ex 416 . . . . . . . . . . . . . . 15 (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 → (𝑦 ∈ (𝑏 ∖ {∅}) → ((𝑓𝑦) ∈ 𝑦 → (𝑦 ∩ ran 𝑓) ≠ ∅)))
6362a2d 29 . . . . . . . . . . . . . 14 (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 → ((𝑦 ∈ (𝑏 ∖ {∅}) → (𝑓𝑦) ∈ 𝑦) → (𝑦 ∈ (𝑏 ∖ {∅}) → (𝑦 ∩ ran 𝑓) ≠ ∅)))
6456, 63syl7 74 . . . . . . . . . . . . 13 (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 → ((𝑦 ∈ (𝑏 ∖ {∅}) → (𝑓𝑦) ∈ 𝑦) → ((𝑦𝑏𝑥𝑦) → (𝑦 ∩ ran 𝑓) ≠ ∅)))
6564exp4a 435 . . . . . . . . . . . 12 (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 → ((𝑦 ∈ (𝑏 ∖ {∅}) → (𝑓𝑦) ∈ 𝑦) → (𝑦𝑏 → (𝑥𝑦 → (𝑦 ∩ ran 𝑓) ≠ ∅))))
6665ralimdv2 3171 . . . . . . . . . . 11 (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 → (∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦 → ∀𝑦𝑏 (𝑥𝑦 → (𝑦 ∩ ran 𝑓) ≠ ∅)))
6766imp 410 . . . . . . . . . 10 ((𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦) → ∀𝑦𝑏 (𝑥𝑦 → (𝑦 ∩ ran 𝑓) ≠ ∅))
6867ad2antlr 726 . . . . . . . . 9 ((((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦)) ∧ 𝑥 𝑏) → ∀𝑦𝑏 (𝑥𝑦 → (𝑦 ∩ ran 𝑓) ≠ ∅))
69 eqidd 2825 . . . . . . . . . 10 ((((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦)) ∧ 𝑥 𝑏) → (topGen‘𝑏) = (topGen‘𝑏))
7051a1i 11 . . . . . . . . . 10 ((((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦)) ∧ 𝑥 𝑏) → 𝑏 = (topGen‘𝑏))
71 simplll 774 . . . . . . . . . 10 ((((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦)) ∧ 𝑥 𝑏) → 𝑏 ∈ TopBases)
7227adantr 484 . . . . . . . . . 10 ((((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦)) ∧ 𝑥 𝑏) → ran 𝑓 𝑏)
73 simpr 488 . . . . . . . . . 10 ((((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦)) ∧ 𝑥 𝑏) → 𝑥 𝑏)
7469, 70, 71, 72, 73elcls3 21686 . . . . . . . . 9 ((((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦)) ∧ 𝑥 𝑏) → (𝑥 ∈ ((cls‘(topGen‘𝑏))‘ran 𝑓) ↔ ∀𝑦𝑏 (𝑥𝑦 → (𝑦 ∩ ran 𝑓) ≠ ∅)))
7568, 74mpbird 260 . . . . . . . 8 ((((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦)) ∧ 𝑥 𝑏) → 𝑥 ∈ ((cls‘(topGen‘𝑏))‘ran 𝑓))
7653, 75eqelssd 3974 . . . . . . 7 (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦)) → ((cls‘(topGen‘𝑏))‘ran 𝑓) = 𝑏)
77 breq1 5056 . . . . . . . . 9 (𝑥 = ran 𝑓 → (𝑥 ≼ ω ↔ ran 𝑓 ≼ ω))
78 fveqeq2 6668 . . . . . . . . 9 (𝑥 = ran 𝑓 → (((cls‘(topGen‘𝑏))‘𝑥) = 𝑏 ↔ ((cls‘(topGen‘𝑏))‘ran 𝑓) = 𝑏))
7977, 78anbi12d 633 . . . . . . . 8 (𝑥 = ran 𝑓 → ((𝑥 ≼ ω ∧ ((cls‘(topGen‘𝑏))‘𝑥) = 𝑏) ↔ (ran 𝑓 ≼ ω ∧ ((cls‘(topGen‘𝑏))‘ran 𝑓) = 𝑏)))
8079rspcev 3609 . . . . . . 7 ((ran 𝑓 ∈ 𝒫 𝑏 ∧ (ran 𝑓 ≼ ω ∧ ((cls‘(topGen‘𝑏))‘ran 𝑓) = 𝑏)) → ∃𝑥 ∈ 𝒫 𝑏(𝑥 ≼ ω ∧ ((cls‘(topGen‘𝑏))‘𝑥) = 𝑏))
8131, 46, 76, 80syl12anc 835 . . . . . 6 (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶ 𝑏 ∧ ∀𝑦 ∈ (𝑏 ∖ {∅})(𝑓𝑦) ∈ 𝑦)) → ∃𝑥 ∈ 𝒫 𝑏(𝑥 ≼ ω ∧ ((cls‘(topGen‘𝑏))‘𝑥) = 𝑏))
8225, 81exlimddv 1937 . . . . 5 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) → ∃𝑥 ∈ 𝒫 𝑏(𝑥 ≼ ω ∧ ((cls‘(topGen‘𝑏))‘𝑥) = 𝑏))
83 unieq 4836 . . . . . . . 8 ((topGen‘𝑏) = 𝐽 (topGen‘𝑏) = 𝐽)
84 2ndcsep.1 . . . . . . . 8 𝑋 = 𝐽
8583, 51, 843eqtr4g 2884 . . . . . . 7 ((topGen‘𝑏) = 𝐽 𝑏 = 𝑋)
8685pweqd 4541 . . . . . 6 ((topGen‘𝑏) = 𝐽 → 𝒫 𝑏 = 𝒫 𝑋)
87 fveq2 6659 . . . . . . . . 9 ((topGen‘𝑏) = 𝐽 → (cls‘(topGen‘𝑏)) = (cls‘𝐽))
8887fveq1d 6661 . . . . . . . 8 ((topGen‘𝑏) = 𝐽 → ((cls‘(topGen‘𝑏))‘𝑥) = ((cls‘𝐽)‘𝑥))
8988, 85eqeq12d 2840 . . . . . . 7 ((topGen‘𝑏) = 𝐽 → (((cls‘(topGen‘𝑏))‘𝑥) = 𝑏 ↔ ((cls‘𝐽)‘𝑥) = 𝑋))
9089anbi2d 631 . . . . . 6 ((topGen‘𝑏) = 𝐽 → ((𝑥 ≼ ω ∧ ((cls‘(topGen‘𝑏))‘𝑥) = 𝑏) ↔ (𝑥 ≼ ω ∧ ((cls‘𝐽)‘𝑥) = 𝑋)))
9186, 90rexeqbidv 3394 . . . . 5 ((topGen‘𝑏) = 𝐽 → (∃𝑥 ∈ 𝒫 𝑏(𝑥 ≼ ω ∧ ((cls‘(topGen‘𝑏))‘𝑥) = 𝑏) ↔ ∃𝑥 ∈ 𝒫 𝑋(𝑥 ≼ ω ∧ ((cls‘𝐽)‘𝑥) = 𝑋)))
9282, 91syl5ibcom 248 . . . 4 ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) → ((topGen‘𝑏) = 𝐽 → ∃𝑥 ∈ 𝒫 𝑋(𝑥 ≼ ω ∧ ((cls‘𝐽)‘𝑥) = 𝑋)))
9392impr 458 . . 3 ((𝑏 ∈ TopBases ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ∃𝑥 ∈ 𝒫 𝑋(𝑥 ≼ ω ∧ ((cls‘𝐽)‘𝑥) = 𝑋))
9493rexlimiva 3274 . 2 (∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽) → ∃𝑥 ∈ 𝒫 𝑋(𝑥 ≼ ω ∧ ((cls‘𝐽)‘𝑥) = 𝑋))
951, 94sylbi 220 1 (𝐽 ∈ 2ndω → ∃𝑥 ∈ 𝒫 𝑋(𝑥 ≼ ω ∧ ((cls‘𝐽)‘𝑥) = 𝑋))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2115   ≠ wne 3014  ∀wral 3133  ∃wrex 3134  Vcvv 3480   ∖ cdif 3916   ∩ cin 3918   ⊆ wss 3919  ∅c0 4276  𝒫 cpw 4522  {csn 4550  ∪ cuni 4825   class class class wbr 5053  dom cdm 5543  ran crn 5544  Oncon0 6179   Fn wfn 6339  ⟶wf 6340  –onto→wfo 6342  ‘cfv 6344  ωcom 7571   ≼ cdom 8499  cardccrd 9357  topGenctg 16709  Topctop 21496  TopBasesctb 21548  clsccl 21621  2ndωc2ndc 22041 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5177  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7452  ax-inf2 9097  ax-cc 9851 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4826  df-int 4864  df-iun 4908  df-iin 4909  df-br 5054  df-opab 5116  df-mpt 5134  df-tr 5160  df-id 5448  df-eprel 5453  df-po 5462  df-so 5463  df-fr 5502  df-se 5503  df-we 5504  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-pred 6136  df-ord 6182  df-on 6183  df-lim 6184  df-suc 6185  df-iota 6303  df-fun 6346  df-fn 6347  df-f 6348  df-f1 6349  df-fo 6350  df-f1o 6351  df-fv 6352  df-isom 6353  df-riota 7104  df-ov 7149  df-oprab 7150  df-mpo 7151  df-om 7572  df-1st 7681  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-er 8281  df-map 8400  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-card 9361  df-acn 9364  df-topgen 16715  df-top 21497  df-bases 21549  df-cld 21622  df-ntr 21623  df-cls 21624  df-2ndc 22043 This theorem is referenced by:  met2ndc  23128
 Copyright terms: Public domain W3C validator