| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . 3
⊢ ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
→ 𝐽 ∈
2ndω) | 
| 2 |  | is2ndc 23454 | . . 3
⊢ (𝐽 ∈ 2ndω
↔ ∃𝑐 ∈
TopBases (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽)) | 
| 3 | 1, 2 | sylib 218 | . 2
⊢ ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
→ ∃𝑐 ∈
TopBases (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽)) | 
| 4 |  | vex 3484 | . . . . . . 7
⊢ 𝑐 ∈ V | 
| 5 | 4, 4 | xpex 7773 | . . . . . 6
⊢ (𝑐 × 𝑐) ∈ V | 
| 6 |  | 3simpa 1149 | . . . . . . . 8
⊢ ((𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐)) | 
| 7 | 6 | ssopab2i 5555 | . . . . . . 7
⊢
{〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣))} ⊆ {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐)} | 
| 8 |  | 2ndcctbss.2 | . . . . . . 7
⊢ 𝑆 = {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣))} | 
| 9 |  | df-xp 5691 | . . . . . . 7
⊢ (𝑐 × 𝑐) = {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐)} | 
| 10 | 7, 8, 9 | 3sstr4i 4035 | . . . . . 6
⊢ 𝑆 ⊆ (𝑐 × 𝑐) | 
| 11 |  | ssdomg 9040 | . . . . . 6
⊢ ((𝑐 × 𝑐) ∈ V → (𝑆 ⊆ (𝑐 × 𝑐) → 𝑆 ≼ (𝑐 × 𝑐))) | 
| 12 | 5, 10, 11 | mp2 9 | . . . . 5
⊢ 𝑆 ≼ (𝑐 × 𝑐) | 
| 13 | 4 | xpdom1 9111 | . . . . . . . . 9
⊢ (𝑐 ≼ ω → (𝑐 × 𝑐) ≼ (ω × 𝑐)) | 
| 14 |  | omex 9683 | . . . . . . . . . 10
⊢ ω
∈ V | 
| 15 | 14 | xpdom2 9107 | . . . . . . . . 9
⊢ (𝑐 ≼ ω → (ω
× 𝑐) ≼ (ω
× ω)) | 
| 16 |  | domtr 9047 | . . . . . . . . 9
⊢ (((𝑐 × 𝑐) ≼ (ω × 𝑐) ∧ (ω × 𝑐) ≼ (ω × ω)) →
(𝑐 × 𝑐) ≼ (ω ×
ω)) | 
| 17 | 13, 15, 16 | syl2anc 584 | . . . . . . . 8
⊢ (𝑐 ≼ ω → (𝑐 × 𝑐) ≼ (ω ×
ω)) | 
| 18 |  | xpomen 10055 | . . . . . . . 8
⊢ (ω
× ω) ≈ ω | 
| 19 |  | domentr 9053 | . . . . . . . 8
⊢ (((𝑐 × 𝑐) ≼ (ω × ω) ∧
(ω × ω) ≈ ω) → (𝑐 × 𝑐) ≼ ω) | 
| 20 | 17, 18, 19 | sylancl 586 | . . . . . . 7
⊢ (𝑐 ≼ ω → (𝑐 × 𝑐) ≼ ω) | 
| 21 | 20 | adantr 480 | . . . . . 6
⊢ ((𝑐 ≼ ω ∧
(topGen‘𝑐) = 𝐽) → (𝑐 × 𝑐) ≼ ω) | 
| 22 | 21 | ad2antll 729 | . . . . 5
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → (𝑐 × 𝑐) ≼ ω) | 
| 23 |  | domtr 9047 | . . . . 5
⊢ ((𝑆 ≼ (𝑐 × 𝑐) ∧ (𝑐 × 𝑐) ≼ ω) → 𝑆 ≼ ω) | 
| 24 | 12, 22, 23 | sylancr 587 | . . . 4
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → 𝑆 ≼
ω) | 
| 25 | 8 | relopabiv 5830 | . . . . . . . . 9
⊢ Rel 𝑆 | 
| 26 |  | simpr 484 | . . . . . . . . 9
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) | 
| 27 |  | 1st2nd 8064 | . . . . . . . . 9
⊢ ((Rel
𝑆 ∧ 𝑥 ∈ 𝑆) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) | 
| 28 | 25, 26, 27 | sylancr 587 | . . . . . . . 8
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ 𝑥 ∈ 𝑆) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) | 
| 29 | 28, 26 | eqeltrrd 2842 | . . . . . . 7
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ 𝑥 ∈ 𝑆) → 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝑆) | 
| 30 |  | df-br 5144 | . . . . . . . . 9
⊢
((1st ‘𝑥)𝑆(2nd ‘𝑥) ↔ 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝑆) | 
| 31 |  | fvex 6919 | . . . . . . . . . 10
⊢
(1st ‘𝑥) ∈ V | 
| 32 |  | fvex 6919 | . . . . . . . . . 10
⊢
(2nd ‘𝑥) ∈ V | 
| 33 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → 𝑢 = (1st ‘𝑥)) | 
| 34 | 33 | eleq1d 2826 | . . . . . . . . . . 11
⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → (𝑢 ∈ 𝑐 ↔ (1st ‘𝑥) ∈ 𝑐)) | 
| 35 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → 𝑣 = (2nd ‘𝑥)) | 
| 36 | 35 | eleq1d 2826 | . . . . . . . . . . 11
⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → (𝑣 ∈ 𝑐 ↔ (2nd ‘𝑥) ∈ 𝑐)) | 
| 37 |  | sseq1 4009 | . . . . . . . . . . . . 13
⊢ (𝑢 = (1st ‘𝑥) → (𝑢 ⊆ 𝑤 ↔ (1st ‘𝑥) ⊆ 𝑤)) | 
| 38 |  | sseq2 4010 | . . . . . . . . . . . . 13
⊢ (𝑣 = (2nd ‘𝑥) → (𝑤 ⊆ 𝑣 ↔ 𝑤 ⊆ (2nd ‘𝑥))) | 
| 39 | 37, 38 | bi2anan9 638 | . . . . . . . . . . . 12
⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → ((𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣) ↔ ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥)))) | 
| 40 | 39 | rexbidv 3179 | . . . . . . . . . . 11
⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → (∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣) ↔ ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥)))) | 
| 41 | 34, 36, 40 | 3anbi123d 1438 | . . . . . . . . . 10
⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → ((𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣)) ↔ ((1st ‘𝑥) ∈ 𝑐 ∧ (2nd ‘𝑥) ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥))))) | 
| 42 | 31, 32, 41, 8 | braba 5542 | . . . . . . . . 9
⊢
((1st ‘𝑥)𝑆(2nd ‘𝑥) ↔ ((1st ‘𝑥) ∈ 𝑐 ∧ (2nd ‘𝑥) ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥)))) | 
| 43 | 30, 42 | bitr3i 277 | . . . . . . . 8
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝑆 ↔ ((1st ‘𝑥) ∈ 𝑐 ∧ (2nd ‘𝑥) ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥)))) | 
| 44 | 43 | simp3bi 1148 | . . . . . . 7
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝑆 → ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥))) | 
| 45 | 29, 44 | syl 17 | . . . . . 6
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ 𝑥 ∈ 𝑆) → ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥))) | 
| 46 |  | fvi 6985 | . . . . . . 7
⊢ (𝐵 ∈ TopBases → ( I
‘𝐵) = 𝐵) | 
| 47 | 46 | ad3antrrr 730 | . . . . . 6
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ 𝑥 ∈ 𝑆) → ( I ‘𝐵) = 𝐵) | 
| 48 | 45, 47 | rexeqtrrdv 3331 | . . . . 5
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ 𝑥 ∈ 𝑆) → ∃𝑤 ∈ ( I ‘𝐵)((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥))) | 
| 49 | 48 | ralrimiva 3146 | . . . 4
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → ∀𝑥 ∈ 𝑆 ∃𝑤 ∈ ( I ‘𝐵)((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥))) | 
| 50 |  | fvex 6919 | . . . . 5
⊢ ( I
‘𝐵) ∈
V | 
| 51 |  | sseq2 4010 | . . . . . 6
⊢ (𝑤 = (𝑓‘𝑥) → ((1st ‘𝑥) ⊆ 𝑤 ↔ (1st ‘𝑥) ⊆ (𝑓‘𝑥))) | 
| 52 |  | sseq1 4009 | . . . . . 6
⊢ (𝑤 = (𝑓‘𝑥) → (𝑤 ⊆ (2nd ‘𝑥) ↔ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) | 
| 53 | 51, 52 | anbi12d 632 | . . . . 5
⊢ (𝑤 = (𝑓‘𝑥) → (((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥)) ↔ ((1st
‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) | 
| 54 | 50, 53 | axcc4dom 10481 | . . . 4
⊢ ((𝑆 ≼ ω ∧
∀𝑥 ∈ 𝑆 ∃𝑤 ∈ ( I ‘𝐵)((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥))) → ∃𝑓(𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) | 
| 55 | 24, 49, 54 | syl2anc 584 | . . 3
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → ∃𝑓(𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) | 
| 56 | 46 | ad2antrr 726 | . . . . . . 7
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → ( I
‘𝐵) = 𝐵) | 
| 57 | 56 | feq3d 6723 | . . . . . 6
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → (𝑓:𝑆⟶( I ‘𝐵) ↔ 𝑓:𝑆⟶𝐵)) | 
| 58 | 57 | anbi1d 631 | . . . . 5
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → ((𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ↔ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))))) | 
| 59 |  | 2ndctop 23455 | . . . . . . . . . . . 12
⊢ (𝐽 ∈ 2ndω
→ 𝐽 ∈
Top) | 
| 60 | 59 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
→ 𝐽 ∈
Top) | 
| 61 | 60 | ad2antrr 726 | . . . . . . . . . 10
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝐽 ∈ Top) | 
| 62 |  | frn 6743 | . . . . . . . . . . . 12
⊢ (𝑓:𝑆⟶𝐵 → ran 𝑓 ⊆ 𝐵) | 
| 63 | 62 | ad2antrl 728 | . . . . . . . . . . 11
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ran 𝑓 ⊆ 𝐵) | 
| 64 |  | bastg 22973 | . . . . . . . . . . . . 13
⊢ (𝐵 ∈ TopBases → 𝐵 ⊆ (topGen‘𝐵)) | 
| 65 | 64 | ad3antrrr 730 | . . . . . . . . . . . 12
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝐵 ⊆ (topGen‘𝐵)) | 
| 66 |  | 2ndcctbss.1 | . . . . . . . . . . . 12
⊢ 𝐽 = (topGen‘𝐵) | 
| 67 | 65, 66 | sseqtrrdi 4025 | . . . . . . . . . . 11
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝐵 ⊆ 𝐽) | 
| 68 | 63, 67 | sstrd 3994 | . . . . . . . . . 10
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ran 𝑓 ⊆ 𝐽) | 
| 69 |  | simprrl 781 | . . . . . . . . . . . . . . 15
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → 𝑜 ∈ 𝐽) | 
| 70 |  | simprr 773 | . . . . . . . . . . . . . . . 16
⊢ ((𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧
(topGen‘𝑐) = 𝐽)) → (topGen‘𝑐) = 𝐽) | 
| 71 | 70 | ad2antlr 727 | . . . . . . . . . . . . . . 15
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → (topGen‘𝑐) = 𝐽) | 
| 72 | 69, 71 | eleqtrrd 2844 | . . . . . . . . . . . . . 14
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → 𝑜 ∈ (topGen‘𝑐)) | 
| 73 |  | simprrr 782 | . . . . . . . . . . . . . 14
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → 𝑡 ∈ 𝑜) | 
| 74 |  | tg2 22972 | . . . . . . . . . . . . . 14
⊢ ((𝑜 ∈ (topGen‘𝑐) ∧ 𝑡 ∈ 𝑜) → ∃𝑑 ∈ 𝑐 (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) | 
| 75 | 72, 73, 74 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → ∃𝑑 ∈ 𝑐 (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) | 
| 76 |  | bastg 22973 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 ∈ TopBases → 𝑐 ⊆ (topGen‘𝑐)) | 
| 77 | 76 | ad2antrl 728 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → 𝑐 ⊆ (topGen‘𝑐)) | 
| 78 | 77 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑐 ⊆ (topGen‘𝑐)) | 
| 79 | 66 | eqeq2i 2750 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((topGen‘𝑐) =
𝐽 ↔
(topGen‘𝑐) =
(topGen‘𝐵)) | 
| 80 | 79 | biimpi 216 | . . . . . . . . . . . . . . . . . . . 20
⊢
((topGen‘𝑐) =
𝐽 →
(topGen‘𝑐) =
(topGen‘𝐵)) | 
| 81 | 80 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑐 ≼ ω ∧
(topGen‘𝑐) = 𝐽) → (topGen‘𝑐) = (topGen‘𝐵)) | 
| 82 | 81 | ad2antll 729 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) →
(topGen‘𝑐) =
(topGen‘𝐵)) | 
| 83 | 82 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → (topGen‘𝑐) = (topGen‘𝐵)) | 
| 84 | 78, 83 | sseqtrd 4020 | . . . . . . . . . . . . . . . 16
⊢
(((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑐 ⊆ (topGen‘𝐵)) | 
| 85 |  | simprl 771 | . . . . . . . . . . . . . . . 16
⊢
(((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑑 ∈ 𝑐) | 
| 86 | 84, 85 | sseldd 3984 | . . . . . . . . . . . . . . 15
⊢
(((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑑 ∈ (topGen‘𝐵)) | 
| 87 |  | simprrl 781 | . . . . . . . . . . . . . . 15
⊢
(((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑡 ∈ 𝑑) | 
| 88 |  | tg2 22972 | . . . . . . . . . . . . . . 15
⊢ ((𝑑 ∈ (topGen‘𝐵) ∧ 𝑡 ∈ 𝑑) → ∃𝑚 ∈ 𝐵 (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑)) | 
| 89 | 86, 87, 88 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢
(((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → ∃𝑚 ∈ 𝐵 (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑)) | 
| 90 | 64 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → 𝐵 ⊆ (topGen‘𝐵)) | 
| 91 | 90 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝐵 ⊆ (topGen‘𝐵)) | 
| 92 | 71 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → (topGen‘𝑐) = 𝐽) | 
| 93 | 92, 66 | eqtr2di 2794 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → (topGen‘𝐵) = (topGen‘𝑐)) | 
| 94 | 91, 93 | sseqtrd 4020 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝐵 ⊆ (topGen‘𝑐)) | 
| 95 |  | simprl 771 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝑚 ∈ 𝐵) | 
| 96 | 94, 95 | sseldd 3984 | . . . . . . . . . . . . . . . 16
⊢
((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝑚 ∈ (topGen‘𝑐)) | 
| 97 |  | simprrl 781 | . . . . . . . . . . . . . . . 16
⊢
((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝑡 ∈ 𝑚) | 
| 98 |  | tg2 22972 | . . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ (topGen‘𝑐) ∧ 𝑡 ∈ 𝑚) → ∃𝑛 ∈ 𝑐 (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚)) | 
| 99 | 96, 97, 98 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢
((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → ∃𝑛 ∈ 𝑐 (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚)) | 
| 100 |  | ffn 6736 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓:𝑆⟶𝐵 → 𝑓 Fn 𝑆) | 
| 101 | 100 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜)) → 𝑓 Fn 𝑆) | 
| 102 | 101 | ad2antlr 727 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑓 Fn 𝑆) | 
| 103 | 102 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢
(((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑓 Fn 𝑆) | 
| 104 |  | simprl 771 | . . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑛 ∈ 𝑐) | 
| 105 | 85 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑑 ∈ 𝑐) | 
| 106 |  | simplrl 777 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑚 ∈ 𝐵) | 
| 107 |  | simprrr 782 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑛 ⊆ 𝑚) | 
| 108 |  | simprr 773 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑)) → 𝑚 ⊆ 𝑑) | 
| 109 | 108 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑚 ⊆ 𝑑) | 
| 110 |  | sseq2 4010 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑚 → (𝑛 ⊆ 𝑤 ↔ 𝑛 ⊆ 𝑚)) | 
| 111 |  | sseq1 4009 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑚 → (𝑤 ⊆ 𝑑 ↔ 𝑚 ⊆ 𝑑)) | 
| 112 | 110, 111 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑚 → ((𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑) ↔ (𝑛 ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑑))) | 
| 113 | 112 | rspcev 3622 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 ∈ 𝐵 ∧ (𝑛 ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑑)) → ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑)) | 
| 114 | 106, 107,
109, 113 | syl12anc 837 | . . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑)) | 
| 115 |  | df-br 5144 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛𝑆𝑑 ↔ 〈𝑛, 𝑑〉 ∈ 𝑆) | 
| 116 |  | vex 3484 | . . . . . . . . . . . . . . . . . . . 20
⊢ 𝑛 ∈ V | 
| 117 |  | vex 3484 | . . . . . . . . . . . . . . . . . . . 20
⊢ 𝑑 ∈ V | 
| 118 |  | simpl 482 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → 𝑢 = 𝑛) | 
| 119 | 118 | eleq1d 2826 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → (𝑢 ∈ 𝑐 ↔ 𝑛 ∈ 𝑐)) | 
| 120 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → 𝑣 = 𝑑) | 
| 121 | 120 | eleq1d 2826 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → (𝑣 ∈ 𝑐 ↔ 𝑑 ∈ 𝑐)) | 
| 122 |  | sseq1 4009 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 = 𝑛 → (𝑢 ⊆ 𝑤 ↔ 𝑛 ⊆ 𝑤)) | 
| 123 |  | sseq2 4010 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑣 = 𝑑 → (𝑤 ⊆ 𝑣 ↔ 𝑤 ⊆ 𝑑)) | 
| 124 | 122, 123 | bi2anan9 638 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → ((𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣) ↔ (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑))) | 
| 125 | 124 | rexbidv 3179 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → (∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣) ↔ ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑))) | 
| 126 | 119, 121,
125 | 3anbi123d 1438 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → ((𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣)) ↔ (𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑)))) | 
| 127 | 116, 117,
126, 8 | braba 5542 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛𝑆𝑑 ↔ (𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑))) | 
| 128 | 115, 127 | bitr3i 277 | . . . . . . . . . . . . . . . . . 18
⊢
(〈𝑛, 𝑑〉 ∈ 𝑆 ↔ (𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑))) | 
| 129 | 104, 105,
114, 128 | syl3anbrc 1344 | . . . . . . . . . . . . . . . . 17
⊢
(((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 〈𝑛, 𝑑〉 ∈ 𝑆) | 
| 130 |  | fnfvelrn 7100 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑓 Fn 𝑆 ∧ 〈𝑛, 𝑑〉 ∈ 𝑆) → (𝑓‘〈𝑛, 𝑑〉) ∈ ran 𝑓) | 
| 131 | 103, 129,
130 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢
(((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → (𝑓‘〈𝑛, 𝑑〉) ∈ ran 𝑓) | 
| 132 |  | simprl 771 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑛 ∈ 𝑐) | 
| 133 |  | simplll 775 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑑 ∈ 𝑐) | 
| 134 |  | simplrl 777 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑚 ∈ 𝐵) | 
| 135 |  | simprrr 782 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑛 ⊆ 𝑚) | 
| 136 | 108 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑚 ⊆ 𝑑) | 
| 137 | 134, 135,
136, 113 | syl12anc 837 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑)) | 
| 138 | 132, 133,
137, 128 | syl3anbrc 1344 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 〈𝑛, 𝑑〉 ∈ 𝑆) | 
| 139 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 〈𝑛, 𝑑〉 → (1st ‘𝑥) = (1st
‘〈𝑛, 𝑑〉)) | 
| 140 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 〈𝑛, 𝑑〉 → (𝑓‘𝑥) = (𝑓‘〈𝑛, 𝑑〉)) | 
| 141 | 139, 140 | sseq12d 4017 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 〈𝑛, 𝑑〉 → ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ↔ (1st ‘〈𝑛, 𝑑〉) ⊆ (𝑓‘〈𝑛, 𝑑〉))) | 
| 142 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 〈𝑛, 𝑑〉 → (2nd ‘𝑥) = (2nd
‘〈𝑛, 𝑑〉)) | 
| 143 | 140, 142 | sseq12d 4017 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 〈𝑛, 𝑑〉 → ((𝑓‘𝑥) ⊆ (2nd ‘𝑥) ↔ (𝑓‘〈𝑛, 𝑑〉) ⊆ (2nd
‘〈𝑛, 𝑑〉))) | 
| 144 | 141, 143 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 〈𝑛, 𝑑〉 → (((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)) ↔ ((1st
‘〈𝑛, 𝑑〉) ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ (2nd
‘〈𝑛, 𝑑〉)))) | 
| 145 | 144 | rspcv 3618 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(〈𝑛, 𝑑〉 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)) → ((1st
‘〈𝑛, 𝑑〉) ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ (2nd
‘〈𝑛, 𝑑〉)))) | 
| 146 | 138, 145 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → (∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)) → ((1st
‘〈𝑛, 𝑑〉) ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ (2nd
‘〈𝑛, 𝑑〉)))) | 
| 147 | 116, 117 | op1st 8022 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(1st ‘〈𝑛, 𝑑〉) = 𝑛 | 
| 148 | 147 | sseq1i 4012 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((1st ‘〈𝑛, 𝑑〉) ⊆ (𝑓‘〈𝑛, 𝑑〉) ↔ 𝑛 ⊆ (𝑓‘〈𝑛, 𝑑〉)) | 
| 149 | 116, 117 | op2nd 8023 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(2nd ‘〈𝑛, 𝑑〉) = 𝑑 | 
| 150 | 149 | sseq2i 4013 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑓‘〈𝑛, 𝑑〉) ⊆ (2nd
‘〈𝑛, 𝑑〉) ↔ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑑) | 
| 151 | 148, 150 | anbi12i 628 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1st ‘〈𝑛, 𝑑〉) ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ (2nd
‘〈𝑛, 𝑑〉)) ↔ (𝑛 ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑑)) | 
| 152 |  | simprl 771 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑑)) → 𝑛 ⊆ (𝑓‘〈𝑛, 𝑑〉)) | 
| 153 |  | simprl 771 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚)) → 𝑡 ∈ 𝑛) | 
| 154 | 153 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑑)) → 𝑡 ∈ 𝑛) | 
| 155 | 152, 154 | sseldd 3984 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑑)) → 𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉)) | 
| 156 |  | simprr 773 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑑)) → (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑑) | 
| 157 |  | simplrr 778 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝑑 ⊆ 𝑜) | 
| 158 | 157 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑑)) → 𝑑 ⊆ 𝑜) | 
| 159 | 156, 158 | sstrd 3994 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑑)) → (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜) | 
| 160 | 155, 159 | jca 511 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑑)) → (𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜)) | 
| 161 | 160 | ex 412 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → ((𝑛 ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑑) → (𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜))) | 
| 162 | 151, 161 | biimtrid 242 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → (((1st
‘〈𝑛, 𝑑〉) ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ (2nd
‘〈𝑛, 𝑑〉)) → (𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜))) | 
| 163 | 146, 162 | syldc 48 | . . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑥 ∈
𝑆 ((1st
‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)) → ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → (𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜))) | 
| 164 | 163 | exp4c 432 | . . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑥 ∈
𝑆 ((1st
‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)) → ((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) → ((𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑)) → ((𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚)) → (𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜))))) | 
| 165 | 164 | ad2antlr 727 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜)) → ((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) → ((𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑)) → ((𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚)) → (𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜))))) | 
| 166 | 165 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → ((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) → ((𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑)) → ((𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚)) → (𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜))))) | 
| 167 | 166 | imp41 425 | . . . . . . . . . . . . . . . 16
⊢
(((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → (𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜)) | 
| 168 |  | eleq2 2830 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (𝑓‘〈𝑛, 𝑑〉) → (𝑡 ∈ 𝑏 ↔ 𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉))) | 
| 169 |  | sseq1 4009 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (𝑓‘〈𝑛, 𝑑〉) → (𝑏 ⊆ 𝑜 ↔ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜)) | 
| 170 | 168, 169 | anbi12d 632 | . . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑓‘〈𝑛, 𝑑〉) → ((𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜) ↔ (𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜))) | 
| 171 | 170 | rspcev 3622 | . . . . . . . . . . . . . . . 16
⊢ (((𝑓‘〈𝑛, 𝑑〉) ∈ ran 𝑓 ∧ (𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜)) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜)) | 
| 172 | 131, 167,
171 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢
(((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜)) | 
| 173 | 99, 172 | rexlimddv 3161 | . . . . . . . . . . . . . 14
⊢
((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜)) | 
| 174 | 89, 173 | rexlimddv 3161 | . . . . . . . . . . . . 13
⊢
(((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜)) | 
| 175 | 75, 174 | rexlimddv 3161 | . . . . . . . . . . . 12
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜)) | 
| 176 | 175 | expr 456 | . . . . . . . . . . 11
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ((𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜))) | 
| 177 | 176 | ralrimivv 3200 | . . . . . . . . . 10
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ∀𝑜 ∈ 𝐽 ∀𝑡 ∈ 𝑜 ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜)) | 
| 178 |  | basgen2 22996 | . . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ ran 𝑓 ⊆ 𝐽 ∧ ∀𝑜 ∈ 𝐽 ∀𝑡 ∈ 𝑜 ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜)) → (topGen‘ran 𝑓) = 𝐽) | 
| 179 | 61, 68, 177, 178 | syl3anc 1373 | . . . . . . . . 9
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → (topGen‘ran
𝑓) = 𝐽) | 
| 180 | 179, 61 | eqeltrd 2841 | . . . . . . . 8
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → (topGen‘ran
𝑓) ∈
Top) | 
| 181 |  | tgclb 22977 | . . . . . . . 8
⊢ (ran
𝑓 ∈ TopBases ↔
(topGen‘ran 𝑓) ∈
Top) | 
| 182 | 180, 181 | sylibr 234 | . . . . . . 7
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ran 𝑓 ∈
TopBases) | 
| 183 |  | omelon 9686 | . . . . . . . . . 10
⊢ ω
∈ On | 
| 184 | 24 | adantr 480 | . . . . . . . . . 10
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝑆 ≼ ω) | 
| 185 |  | ondomen 10077 | . . . . . . . . . 10
⊢ ((ω
∈ On ∧ 𝑆 ≼
ω) → 𝑆 ∈
dom card) | 
| 186 | 183, 184,
185 | sylancr 587 | . . . . . . . . 9
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝑆 ∈ dom card) | 
| 187 | 100 | ad2antrl 728 | . . . . . . . . . 10
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝑓 Fn 𝑆) | 
| 188 |  | dffn4 6826 | . . . . . . . . . 10
⊢ (𝑓 Fn 𝑆 ↔ 𝑓:𝑆–onto→ran 𝑓) | 
| 189 | 187, 188 | sylib 218 | . . . . . . . . 9
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝑓:𝑆–onto→ran 𝑓) | 
| 190 |  | fodomnum 10097 | . . . . . . . . 9
⊢ (𝑆 ∈ dom card → (𝑓:𝑆–onto→ran 𝑓 → ran 𝑓 ≼ 𝑆)) | 
| 191 | 186, 189,
190 | sylc 65 | . . . . . . . 8
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ran 𝑓 ≼ 𝑆) | 
| 192 |  | domtr 9047 | . . . . . . . 8
⊢ ((ran
𝑓 ≼ 𝑆 ∧ 𝑆 ≼ ω) → ran 𝑓 ≼
ω) | 
| 193 | 191, 184,
192 | syl2anc 584 | . . . . . . 7
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ran 𝑓 ≼
ω) | 
| 194 | 179 | eqcomd 2743 | . . . . . . 7
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝐽 = (topGen‘ran 𝑓)) | 
| 195 |  | breq1 5146 | . . . . . . . . 9
⊢ (𝑏 = ran 𝑓 → (𝑏 ≼ ω ↔ ran 𝑓 ≼
ω)) | 
| 196 |  | sseq1 4009 | . . . . . . . . 9
⊢ (𝑏 = ran 𝑓 → (𝑏 ⊆ 𝐵 ↔ ran 𝑓 ⊆ 𝐵)) | 
| 197 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑏 = ran 𝑓 → (topGen‘𝑏) = (topGen‘ran 𝑓)) | 
| 198 | 197 | eqeq2d 2748 | . . . . . . . . 9
⊢ (𝑏 = ran 𝑓 → (𝐽 = (topGen‘𝑏) ↔ 𝐽 = (topGen‘ran 𝑓))) | 
| 199 | 195, 196,
198 | 3anbi123d 1438 | . . . . . . . 8
⊢ (𝑏 = ran 𝑓 → ((𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏)) ↔ (ran 𝑓 ≼ ω ∧ ran 𝑓 ⊆ 𝐵 ∧ 𝐽 = (topGen‘ran 𝑓)))) | 
| 200 | 199 | rspcev 3622 | . . . . . . 7
⊢ ((ran
𝑓 ∈ TopBases ∧
(ran 𝑓 ≼ ω
∧ ran 𝑓 ⊆ 𝐵 ∧ 𝐽 = (topGen‘ran 𝑓))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏))) | 
| 201 | 182, 193,
63, 194, 200 | syl13anc 1374 | . . . . . 6
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏))) | 
| 202 | 201 | ex 412 | . . . . 5
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏)))) | 
| 203 | 58, 202 | sylbid 240 | . . . 4
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → ((𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏)))) | 
| 204 | 203 | exlimdv 1933 | . . 3
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → (∃𝑓(𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏)))) | 
| 205 | 55, 204 | mpd 15 | . 2
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏))) | 
| 206 | 3, 205 | rexlimddv 3161 | 1
⊢ ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
→ ∃𝑏 ∈
TopBases (𝑏 ≼ ω
∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏))) |