Metamath Proof Explorer

Theorem 2ndcsep

Description: A second-countable topology is separable, which is to say it contains a countable dense subset. (Contributed by Mario Carneiro, 13-Apr-2015)

Ref Expression
Hypothesis 2ndcsep.1 ⊢ 𝑋 = ∪ 𝐽
Assertion 2ndcsep ( 𝐽 ∈ 2ndω → ∃ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = 𝑋 ) )

Proof

Step Hyp Ref Expression
1 2ndcsep.1 ⊢ 𝑋 = ∪ 𝐽
2 is2ndc ⊢ ( 𝐽 ∈ 2ndω ↔ ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) )
3 vex ⊢ 𝑏 ∈ V
4 difss ⊢ ( 𝑏 ∖ { ∅ } ) ⊆ 𝑏
5 ssdomg ⊢ ( 𝑏 ∈ V → ( ( 𝑏 ∖ { ∅ } ) ⊆ 𝑏 → ( 𝑏 ∖ { ∅ } ) ≼ 𝑏 ) )
6 3 4 5 mp2 ⊢ ( 𝑏 ∖ { ∅ } ) ≼ 𝑏
7 simpr ⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) → 𝑏 ≼ ω )
8 domtr ⊢ ( ( ( 𝑏 ∖ { ∅ } ) ≼ 𝑏 ∧ 𝑏 ≼ ω ) → ( 𝑏 ∖ { ∅ } ) ≼ ω )
9 6 7 8 sylancr ⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) → ( 𝑏 ∖ { ∅ } ) ≼ ω )
10 eldifsn ⊢ ( 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ↔ ( 𝑦 ∈ 𝑏 ∧ 𝑦 ≠ ∅ ) )
11 n0 ⊢ ( 𝑦 ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ 𝑦 )
12 elunii ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑏 ) → 𝑧 ∈ ∪ 𝑏 )
13 simpl ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑏 ) → 𝑧 ∈ 𝑦 )
14 12 13 jca ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑏 ) → ( 𝑧 ∈ ∪ 𝑏 ∧ 𝑧 ∈ 𝑦 ) )
15 14 expcom ⊢ ( 𝑦 ∈ 𝑏 → ( 𝑧 ∈ 𝑦 → ( 𝑧 ∈ ∪ 𝑏 ∧ 𝑧 ∈ 𝑦 ) ) )
16 15 eximdv ⊢ ( 𝑦 ∈ 𝑏 → ( ∃ 𝑧 𝑧 ∈ 𝑦 → ∃ 𝑧 ( 𝑧 ∈ ∪ 𝑏 ∧ 𝑧 ∈ 𝑦 ) ) )
17 16 imp ⊢ ( ( 𝑦 ∈ 𝑏 ∧ ∃ 𝑧 𝑧 ∈ 𝑦 ) → ∃ 𝑧 ( 𝑧 ∈ ∪ 𝑏 ∧ 𝑧 ∈ 𝑦 ) )
18 df-rex ⊢ ( ∃ 𝑧 ∈ ∪ 𝑏 𝑧 ∈ 𝑦 ↔ ∃ 𝑧 ( 𝑧 ∈ ∪ 𝑏 ∧ 𝑧 ∈ 𝑦 ) )
19 17 18 sylibr ⊢ ( ( 𝑦 ∈ 𝑏 ∧ ∃ 𝑧 𝑧 ∈ 𝑦 ) → ∃ 𝑧 ∈ ∪ 𝑏 𝑧 ∈ 𝑦 )
20 11 19 sylan2b ⊢ ( ( 𝑦 ∈ 𝑏 ∧ 𝑦 ≠ ∅ ) → ∃ 𝑧 ∈ ∪ 𝑏 𝑧 ∈ 𝑦 )
21 10 20 sylbi ⊢ ( 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) → ∃ 𝑧 ∈ ∪ 𝑏 𝑧 ∈ 𝑦 )
22 21 rgen ⊢ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ∃ 𝑧 ∈ ∪ 𝑏 𝑧 ∈ 𝑦
23 vuniex ⊢ ∪ 𝑏 ∈ V
24 eleq1 ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑦 ) → ( 𝑧 ∈ 𝑦 ↔ ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) )
25 23 24 axcc4dom ⊢ ( ( ( 𝑏 ∖ { ∅ } ) ≼ ω ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ∃ 𝑧 ∈ ∪ 𝑏 𝑧 ∈ 𝑦 ) → ∃ 𝑓 ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) )
26 9 22 25 sylancl ⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) → ∃ 𝑓 ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) )
27 frn ⊢ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 → ran 𝑓 ⊆ ∪ 𝑏 )
28 27 ad2antrl ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) ∧ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) → ran 𝑓 ⊆ ∪ 𝑏 )
29 vex ⊢ 𝑓 ∈ V
30 29 rnex ⊢ ran 𝑓 ∈ V
31 30 elpw ⊢ ( ran 𝑓 ∈ 𝒫 ∪ 𝑏 ↔ ran 𝑓 ⊆ ∪ 𝑏 )
32 28 31 sylibr ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) ∧ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) → ran 𝑓 ∈ 𝒫 ∪ 𝑏 )
33 omelon ⊢ ω ∈ On
34 7 adantr ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) ∧ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) → 𝑏 ≼ ω )
35 ondomen ⊢ ( ( ω ∈ On ∧ 𝑏 ≼ ω ) → 𝑏 ∈ dom card )
36 33 34 35 sylancr ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) ∧ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) → 𝑏 ∈ dom card )
37 ssnum ⊢ ( ( 𝑏 ∈ dom card ∧ ( 𝑏 ∖ { ∅ } ) ⊆ 𝑏 ) → ( 𝑏 ∖ { ∅ } ) ∈ dom card )
38 36 4 37 sylancl ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) ∧ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) → ( 𝑏 ∖ { ∅ } ) ∈ dom card )
39 ffn ⊢ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 → 𝑓 Fn ( 𝑏 ∖ { ∅ } ) )
40 39 ad2antrl ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) ∧ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) → 𝑓 Fn ( 𝑏 ∖ { ∅ } ) )
41 dffn4 ⊢ ( 𝑓 Fn ( 𝑏 ∖ { ∅ } ) ↔ 𝑓 : ( 𝑏 ∖ { ∅ } ) –onto→ ran 𝑓 )
42 40 41 sylib ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) ∧ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) → 𝑓 : ( 𝑏 ∖ { ∅ } ) –onto→ ran 𝑓 )
43 fodomnum ⊢ ( ( 𝑏 ∖ { ∅ } ) ∈ dom card → ( 𝑓 : ( 𝑏 ∖ { ∅ } ) –onto→ ran 𝑓 → ran 𝑓 ≼ ( 𝑏 ∖ { ∅ } ) ) )
44 38 42 43 sylc ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) ∧ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) → ran 𝑓 ≼ ( 𝑏 ∖ { ∅ } ) )
45 9 adantr ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) ∧ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) → ( 𝑏 ∖ { ∅ } ) ≼ ω )
46 domtr ⊢ ( ( ran 𝑓 ≼ ( 𝑏 ∖ { ∅ } ) ∧ ( 𝑏 ∖ { ∅ } ) ≼ ω ) → ran 𝑓 ≼ ω )
47 44 45 46 syl2anc ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) ∧ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) → ran 𝑓 ≼ ω )
48 tgcl ⊢ ( 𝑏 ∈ TopBases → ( topGen ‘ 𝑏 ) ∈ Top )
49 48 ad2antrr ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) ∧ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) → ( topGen ‘ 𝑏 ) ∈ Top )
50 unitg ⊢ ( 𝑏 ∈ V → ∪ ( topGen ‘ 𝑏 ) = ∪ 𝑏 )
51 50 elv ⊢ ∪ ( topGen ‘ 𝑏 ) = ∪ 𝑏
52 51 eqcomi ⊢ ∪ 𝑏 = ∪ ( topGen ‘ 𝑏 )
53 52 clsss3 ⊢ ( ( ( topGen ‘ 𝑏 ) ∈ Top ∧ ran 𝑓 ⊆ ∪ 𝑏 ) → ( ( cls ‘ ( topGen ‘ 𝑏 ) ) ‘ ran 𝑓 ) ⊆ ∪ 𝑏 )
54 49 28 53 syl2anc ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) ∧ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) → ( ( cls ‘ ( topGen ‘ 𝑏 ) ) ‘ ran 𝑓 ) ⊆ ∪ 𝑏 )
55 ne0i ⊢ ( 𝑥 ∈ 𝑦 → 𝑦 ≠ ∅ )
56 55 anim2i ⊢ ( ( 𝑦 ∈ 𝑏 ∧ 𝑥 ∈ 𝑦 ) → ( 𝑦 ∈ 𝑏 ∧ 𝑦 ≠ ∅ ) )
57 56 10 sylibr ⊢ ( ( 𝑦 ∈ 𝑏 ∧ 𝑥 ∈ 𝑦 ) → 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) )
58 fnfvelrn ⊢ ( ( 𝑓 Fn ( 𝑏 ∖ { ∅ } ) ∧ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ) → ( 𝑓 ‘ 𝑦 ) ∈ ran 𝑓 )
59 39 58 sylan ⊢ ( ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ) → ( 𝑓 ‘ 𝑦 ) ∈ ran 𝑓 )
60 inelcm ⊢ ( ( ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ∧ ( 𝑓 ‘ 𝑦 ) ∈ ran 𝑓 ) → ( 𝑦 ∩ ran 𝑓 ) ≠ ∅ )
61 60 expcom ⊢ ( ( 𝑓 ‘ 𝑦 ) ∈ ran 𝑓 → ( ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 → ( 𝑦 ∩ ran 𝑓 ) ≠ ∅ ) )
62 59 61 syl ⊢ ( ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ) → ( ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 → ( 𝑦 ∩ ran 𝑓 ) ≠ ∅ ) )
63 62 ex ⊢ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 → ( 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) → ( ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 → ( 𝑦 ∩ ran 𝑓 ) ≠ ∅ ) ) )
64 63 a2d ⊢ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 → ( ( 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) → ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → ( 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) → ( 𝑦 ∩ ran 𝑓 ) ≠ ∅ ) ) )
65 57 64 syl7 ⊢ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 → ( ( 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) → ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → ( ( 𝑦 ∈ 𝑏 ∧ 𝑥 ∈ 𝑦 ) → ( 𝑦 ∩ ran 𝑓 ) ≠ ∅ ) ) )
66 65 exp4a ⊢ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 → ( ( 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) → ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → ( 𝑦 ∈ 𝑏 → ( 𝑥 ∈ 𝑦 → ( 𝑦 ∩ ran 𝑓 ) ≠ ∅ ) ) ) )
67 66 ralimdv2 ⊢ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 → ( ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 → ∀ 𝑦 ∈ 𝑏 ( 𝑥 ∈ 𝑦 → ( 𝑦 ∩ ran 𝑓 ) ≠ ∅ ) ) )
68 67 imp ⊢ ( ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → ∀ 𝑦 ∈ 𝑏 ( 𝑥 ∈ 𝑦 → ( 𝑦 ∩ ran 𝑓 ) ≠ ∅ ) )
69 68 ad2antlr ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) ∧ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) ∧ 𝑥 ∈ ∪ 𝑏 ) → ∀ 𝑦 ∈ 𝑏 ( 𝑥 ∈ 𝑦 → ( 𝑦 ∩ ran 𝑓 ) ≠ ∅ ) )
70 eqidd ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) ∧ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) ∧ 𝑥 ∈ ∪ 𝑏 ) → ( topGen ‘ 𝑏 ) = ( topGen ‘ 𝑏 ) )
71 52 a1i ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) ∧ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) ∧ 𝑥 ∈ ∪ 𝑏 ) → ∪ 𝑏 = ∪ ( topGen ‘ 𝑏 ) )
72 simplll ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) ∧ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) ∧ 𝑥 ∈ ∪ 𝑏 ) → 𝑏 ∈ TopBases )
73 28 adantr ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) ∧ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) ∧ 𝑥 ∈ ∪ 𝑏 ) → ran 𝑓 ⊆ ∪ 𝑏 )
74 simpr ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) ∧ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) ∧ 𝑥 ∈ ∪ 𝑏 ) → 𝑥 ∈ ∪ 𝑏 )
75 70 71 72 73 74 elcls3 ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) ∧ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) ∧ 𝑥 ∈ ∪ 𝑏 ) → ( 𝑥 ∈ ( ( cls ‘ ( topGen ‘ 𝑏 ) ) ‘ ran 𝑓 ) ↔ ∀ 𝑦 ∈ 𝑏 ( 𝑥 ∈ 𝑦 → ( 𝑦 ∩ ran 𝑓 ) ≠ ∅ ) ) )
76 69 75 mpbird ⊢ ( ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) ∧ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) ∧ 𝑥 ∈ ∪ 𝑏 ) → 𝑥 ∈ ( ( cls ‘ ( topGen ‘ 𝑏 ) ) ‘ ran 𝑓 ) )
77 54 76 eqelssd ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) ∧ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) → ( ( cls ‘ ( topGen ‘ 𝑏 ) ) ‘ ran 𝑓 ) = ∪ 𝑏 )
78 breq1 ⊢ ( 𝑥 = ran 𝑓 → ( 𝑥 ≼ ω ↔ ran 𝑓 ≼ ω ) )
79 fveqeq2 ⊢ ( 𝑥 = ran 𝑓 → ( ( ( cls ‘ ( topGen ‘ 𝑏 ) ) ‘ 𝑥 ) = ∪ 𝑏 ↔ ( ( cls ‘ ( topGen ‘ 𝑏 ) ) ‘ ran 𝑓 ) = ∪ 𝑏 ) )
80 78 79 anbi12d ⊢ ( 𝑥 = ran 𝑓 → ( ( 𝑥 ≼ ω ∧ ( ( cls ‘ ( topGen ‘ 𝑏 ) ) ‘ 𝑥 ) = ∪ 𝑏 ) ↔ ( ran 𝑓 ≼ ω ∧ ( ( cls ‘ ( topGen ‘ 𝑏 ) ) ‘ ran 𝑓 ) = ∪ 𝑏 ) ) )
81 80 rspcev ⊢ ( ( ran 𝑓 ∈ 𝒫 ∪ 𝑏 ∧ ( ran 𝑓 ≼ ω ∧ ( ( cls ‘ ( topGen ‘ 𝑏 ) ) ‘ ran 𝑓 ) = ∪ 𝑏 ) ) → ∃ 𝑥 ∈ 𝒫 ∪ 𝑏 ( 𝑥 ≼ ω ∧ ( ( cls ‘ ( topGen ‘ 𝑏 ) ) ‘ 𝑥 ) = ∪ 𝑏 ) )
82 32 47 77 81 syl12anc ⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) ∧ ( 𝑓 : ( 𝑏 ∖ { ∅ } ) ⟶ ∪ 𝑏 ∧ ∀ 𝑦 ∈ ( 𝑏 ∖ { ∅ } ) ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) → ∃ 𝑥 ∈ 𝒫 ∪ 𝑏 ( 𝑥 ≼ ω ∧ ( ( cls ‘ ( topGen ‘ 𝑏 ) ) ‘ 𝑥 ) = ∪ 𝑏 ) )
83 26 82 exlimddv ⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) → ∃ 𝑥 ∈ 𝒫 ∪ 𝑏 ( 𝑥 ≼ ω ∧ ( ( cls ‘ ( topGen ‘ 𝑏 ) ) ‘ 𝑥 ) = ∪ 𝑏 ) )
84 unieq ⊢ ( ( topGen ‘ 𝑏 ) = 𝐽 → ∪ ( topGen ‘ 𝑏 ) = ∪ 𝐽 )
85 84 52 1 3eqtr4g ⊢ ( ( topGen ‘ 𝑏 ) = 𝐽 → ∪ 𝑏 = 𝑋 )
86 85 pweqd ⊢ ( ( topGen ‘ 𝑏 ) = 𝐽 → 𝒫 ∪ 𝑏 = 𝒫 𝑋 )
87 fveq2 ⊢ ( ( topGen ‘ 𝑏 ) = 𝐽 → ( cls ‘ ( topGen ‘ 𝑏 ) ) = ( cls ‘ 𝐽 ) )
88 87 fveq1d ⊢ ( ( topGen ‘ 𝑏 ) = 𝐽 → ( ( cls ‘ ( topGen ‘ 𝑏 ) ) ‘ 𝑥 ) = ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) )
89 88 85 eqeq12d ⊢ ( ( topGen ‘ 𝑏 ) = 𝐽 → ( ( ( cls ‘ ( topGen ‘ 𝑏 ) ) ‘ 𝑥 ) = ∪ 𝑏 ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = 𝑋 ) )
90 89 anbi2d ⊢ ( ( topGen ‘ 𝑏 ) = 𝐽 → ( ( 𝑥 ≼ ω ∧ ( ( cls ‘ ( topGen ‘ 𝑏 ) ) ‘ 𝑥 ) = ∪ 𝑏 ) ↔ ( 𝑥 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = 𝑋 ) ) )
91 86 90 rexeqbidv ⊢ ( ( topGen ‘ 𝑏 ) = 𝐽 → ( ∃ 𝑥 ∈ 𝒫 ∪ 𝑏 ( 𝑥 ≼ ω ∧ ( ( cls ‘ ( topGen ‘ 𝑏 ) ) ‘ 𝑥 ) = ∪ 𝑏 ) ↔ ∃ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = 𝑋 ) ) )
92 83 91 syl5ibcom ⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) → ( ( topGen ‘ 𝑏 ) = 𝐽 → ∃ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = 𝑋 ) ) )
93 92 impr ⊢ ( ( 𝑏 ∈ TopBases ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) → ∃ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = 𝑋 ) )
94 93 rexlimiva ⊢ ( ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) → ∃ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = 𝑋 ) )
95 2 94 sylbi ⊢ ( 𝐽 ∈ 2ndω → ∃ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = 𝑋 ) )