| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | is2ndc 23455 | . . 3
⊢ (𝐽 ∈ 2ndω
↔ ∃𝑥 ∈
TopBases (𝑥 ≼ ω
∧ (topGen‘𝑥) =
𝐽)) | 
| 2 |  | df-rex 3070 | . . . 4
⊢
(∃𝑥 ∈
TopBases (𝑥 ≼ ω
∧ (topGen‘𝑥) =
𝐽) ↔ ∃𝑥(𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝐽))) | 
| 3 |  | simprl 770 | . . . . . 6
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → 𝑥 ≼ ω) | 
| 4 |  | ssfii 9460 | . . . . . . . 8
⊢ (𝑥 ∈ TopBases → 𝑥 ⊆ (fi‘𝑥)) | 
| 5 |  | fvex 6918 | . . . . . . . . . 10
⊢
(topGen‘𝑥)
∈ V | 
| 6 |  | bastg 22974 | . . . . . . . . . . 11
⊢ (𝑥 ∈ TopBases → 𝑥 ⊆ (topGen‘𝑥)) | 
| 7 | 6 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → 𝑥 ⊆ (topGen‘𝑥)) | 
| 8 |  | fiss 9465 | . . . . . . . . . 10
⊢
(((topGen‘𝑥)
∈ V ∧ 𝑥 ⊆
(topGen‘𝑥)) →
(fi‘𝑥) ⊆
(fi‘(topGen‘𝑥))) | 
| 9 | 5, 7, 8 | sylancr 587 | . . . . . . . . 9
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → (fi‘𝑥) ⊆
(fi‘(topGen‘𝑥))) | 
| 10 |  | tgcl 22977 | . . . . . . . . . . 11
⊢ (𝑥 ∈ TopBases →
(topGen‘𝑥) ∈
Top) | 
| 11 | 10 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → (topGen‘𝑥) ∈ Top) | 
| 12 |  | fitop 22907 | . . . . . . . . . 10
⊢
((topGen‘𝑥)
∈ Top → (fi‘(topGen‘𝑥)) = (topGen‘𝑥)) | 
| 13 | 11, 12 | syl 17 | . . . . . . . . 9
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) →
(fi‘(topGen‘𝑥))
= (topGen‘𝑥)) | 
| 14 | 9, 13 | sseqtrd 4019 | . . . . . . . 8
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → (fi‘𝑥) ⊆ (topGen‘𝑥)) | 
| 15 |  | 2basgen 22998 | . . . . . . . 8
⊢ ((𝑥 ⊆ (fi‘𝑥) ∧ (fi‘𝑥) ⊆ (topGen‘𝑥)) → (topGen‘𝑥) =
(topGen‘(fi‘𝑥))) | 
| 16 | 4, 14, 15 | syl2an2r 685 | . . . . . . 7
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → (topGen‘𝑥) =
(topGen‘(fi‘𝑥))) | 
| 17 |  | simprr 772 | . . . . . . 7
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → (topGen‘𝑥) = 𝐽) | 
| 18 | 16, 17 | eqtr3d 2778 | . . . . . 6
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) →
(topGen‘(fi‘𝑥))
= 𝐽) | 
| 19 | 3, 18 | jca 511 | . . . . 5
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → (𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽)) | 
| 20 | 19 | eximi 1834 | . . . 4
⊢
(∃𝑥(𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → ∃𝑥(𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽)) | 
| 21 | 2, 20 | sylbi 217 | . . 3
⊢
(∃𝑥 ∈
TopBases (𝑥 ≼ ω
∧ (topGen‘𝑥) =
𝐽) → ∃𝑥(𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽)) | 
| 22 | 1, 21 | sylbi 217 | . 2
⊢ (𝐽 ∈ 2ndω
→ ∃𝑥(𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽)) | 
| 23 |  | fibas 22985 | . . . . 5
⊢
(fi‘𝑥) ∈
TopBases | 
| 24 |  | simpl 482 | . . . . . . 7
⊢ ((𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽) → 𝑥 ≼
ω) | 
| 25 |  | fictb 10285 | . . . . . . . 8
⊢ (𝑥 ∈ V → (𝑥 ≼ ω ↔
(fi‘𝑥) ≼
ω)) | 
| 26 | 25 | elv 3484 | . . . . . . 7
⊢ (𝑥 ≼ ω ↔
(fi‘𝑥) ≼
ω) | 
| 27 | 24, 26 | sylib 218 | . . . . . 6
⊢ ((𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽) → (fi‘𝑥) ≼
ω) | 
| 28 |  | simpr 484 | . . . . . 6
⊢ ((𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽) →
(topGen‘(fi‘𝑥))
= 𝐽) | 
| 29 | 27, 28 | jca 511 | . . . . 5
⊢ ((𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽) →
((fi‘𝑥) ≼
ω ∧ (topGen‘(fi‘𝑥)) = 𝐽)) | 
| 30 |  | breq1 5145 | . . . . . . 7
⊢ (𝑦 = (fi‘𝑥) → (𝑦 ≼ ω ↔ (fi‘𝑥) ≼
ω)) | 
| 31 |  | fveqeq2 6914 | . . . . . . 7
⊢ (𝑦 = (fi‘𝑥) → ((topGen‘𝑦) = 𝐽 ↔ (topGen‘(fi‘𝑥)) = 𝐽)) | 
| 32 | 30, 31 | anbi12d 632 | . . . . . 6
⊢ (𝑦 = (fi‘𝑥) → ((𝑦 ≼ ω ∧ (topGen‘𝑦) = 𝐽) ↔ ((fi‘𝑥) ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽))) | 
| 33 | 32 | rspcev 3621 | . . . . 5
⊢
(((fi‘𝑥)
∈ TopBases ∧ ((fi‘𝑥) ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽)) → ∃𝑦 ∈ TopBases (𝑦 ≼ ω ∧
(topGen‘𝑦) = 𝐽)) | 
| 34 | 23, 29, 33 | sylancr 587 | . . . 4
⊢ ((𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽) → ∃𝑦 ∈ TopBases (𝑦 ≼ ω ∧
(topGen‘𝑦) = 𝐽)) | 
| 35 |  | is2ndc 23455 | . . . 4
⊢ (𝐽 ∈ 2ndω
↔ ∃𝑦 ∈
TopBases (𝑦 ≼ ω
∧ (topGen‘𝑦) =
𝐽)) | 
| 36 | 34, 35 | sylibr 234 | . . 3
⊢ ((𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽) → 𝐽 ∈
2ndω) | 
| 37 | 36 | exlimiv 1929 | . 2
⊢
(∃𝑥(𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽) → 𝐽 ∈
2ndω) | 
| 38 | 22, 37 | impbii 209 | 1
⊢ (𝐽 ∈ 2ndω
↔ ∃𝑥(𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽)) |