Step | Hyp | Ref
| Expression |
1 | | is2ndc 21059 |
. . 3
⊢ (𝐽 ∈ 2nd𝜔
↔ ∃𝑥 ∈
TopBases (𝑥 ≼ ω
∧ (topGen‘𝑥) =
𝐽)) |
2 | | df-rex 2902 |
. . . 4
⊢
(∃𝑥 ∈
TopBases (𝑥 ≼ ω
∧ (topGen‘𝑥) =
𝐽) ↔ ∃𝑥(𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝐽))) |
3 | | simprl 790 |
. . . . . 6
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → 𝑥 ≼ ω) |
4 | | ssfii 8208 |
. . . . . . . . 9
⊢ (𝑥 ∈ TopBases → 𝑥 ⊆ (fi‘𝑥)) |
5 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → 𝑥 ⊆ (fi‘𝑥)) |
6 | | fvex 6113 |
. . . . . . . . . 10
⊢
(topGen‘𝑥)
∈ V |
7 | | bastg 20581 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ TopBases → 𝑥 ⊆ (topGen‘𝑥)) |
8 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → 𝑥 ⊆ (topGen‘𝑥)) |
9 | | fiss 8213 |
. . . . . . . . . 10
⊢
(((topGen‘𝑥)
∈ V ∧ 𝑥 ⊆
(topGen‘𝑥)) →
(fi‘𝑥) ⊆
(fi‘(topGen‘𝑥))) |
10 | 6, 8, 9 | sylancr 694 |
. . . . . . . . 9
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → (fi‘𝑥) ⊆
(fi‘(topGen‘𝑥))) |
11 | | tgcl 20584 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ TopBases →
(topGen‘𝑥) ∈
Top) |
12 | 11 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → (topGen‘𝑥) ∈ Top) |
13 | | fitop 20530 |
. . . . . . . . . 10
⊢
((topGen‘𝑥)
∈ Top → (fi‘(topGen‘𝑥)) = (topGen‘𝑥)) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) →
(fi‘(topGen‘𝑥))
= (topGen‘𝑥)) |
15 | 10, 14 | sseqtrd 3604 |
. . . . . . . 8
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → (fi‘𝑥) ⊆ (topGen‘𝑥)) |
16 | | 2basgen 20605 |
. . . . . . . 8
⊢ ((𝑥 ⊆ (fi‘𝑥) ∧ (fi‘𝑥) ⊆ (topGen‘𝑥)) → (topGen‘𝑥) =
(topGen‘(fi‘𝑥))) |
17 | 5, 15, 16 | syl2anc 691 |
. . . . . . 7
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → (topGen‘𝑥) =
(topGen‘(fi‘𝑥))) |
18 | | simprr 792 |
. . . . . . 7
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → (topGen‘𝑥) = 𝐽) |
19 | 17, 18 | eqtr3d 2646 |
. . . . . 6
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) →
(topGen‘(fi‘𝑥))
= 𝐽) |
20 | 3, 19 | jca 553 |
. . . . 5
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → (𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽)) |
21 | 20 | eximi 1752 |
. . . 4
⊢
(∃𝑥(𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → ∃𝑥(𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽)) |
22 | 2, 21 | sylbi 206 |
. . 3
⊢
(∃𝑥 ∈
TopBases (𝑥 ≼ ω
∧ (topGen‘𝑥) =
𝐽) → ∃𝑥(𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽)) |
23 | 1, 22 | sylbi 206 |
. 2
⊢ (𝐽 ∈ 2nd𝜔
→ ∃𝑥(𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽)) |
24 | | fibas 20592 |
. . . . 5
⊢
(fi‘𝑥) ∈
TopBases |
25 | | simpl 472 |
. . . . . . 7
⊢ ((𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽) → 𝑥 ≼
ω) |
26 | | vex 3176 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
27 | | fictb 8950 |
. . . . . . . 8
⊢ (𝑥 ∈ V → (𝑥 ≼ ω ↔
(fi‘𝑥) ≼
ω)) |
28 | 26, 27 | ax-mp 5 |
. . . . . . 7
⊢ (𝑥 ≼ ω ↔
(fi‘𝑥) ≼
ω) |
29 | 25, 28 | sylib 207 |
. . . . . 6
⊢ ((𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽) → (fi‘𝑥) ≼
ω) |
30 | | simpr 476 |
. . . . . 6
⊢ ((𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽) →
(topGen‘(fi‘𝑥))
= 𝐽) |
31 | 29, 30 | jca 553 |
. . . . 5
⊢ ((𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽) →
((fi‘𝑥) ≼
ω ∧ (topGen‘(fi‘𝑥)) = 𝐽)) |
32 | | breq1 4586 |
. . . . . . 7
⊢ (𝑦 = (fi‘𝑥) → (𝑦 ≼ ω ↔ (fi‘𝑥) ≼
ω)) |
33 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑦 = (fi‘𝑥) → (topGen‘𝑦) = (topGen‘(fi‘𝑥))) |
34 | 33 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑦 = (fi‘𝑥) → ((topGen‘𝑦) = 𝐽 ↔ (topGen‘(fi‘𝑥)) = 𝐽)) |
35 | 32, 34 | anbi12d 743 |
. . . . . 6
⊢ (𝑦 = (fi‘𝑥) → ((𝑦 ≼ ω ∧ (topGen‘𝑦) = 𝐽) ↔ ((fi‘𝑥) ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽))) |
36 | 35 | rspcev 3282 |
. . . . 5
⊢
(((fi‘𝑥)
∈ TopBases ∧ ((fi‘𝑥) ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽)) → ∃𝑦 ∈ TopBases (𝑦 ≼ ω ∧
(topGen‘𝑦) = 𝐽)) |
37 | 24, 31, 36 | sylancr 694 |
. . . 4
⊢ ((𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽) → ∃𝑦 ∈ TopBases (𝑦 ≼ ω ∧
(topGen‘𝑦) = 𝐽)) |
38 | | is2ndc 21059 |
. . . 4
⊢ (𝐽 ∈ 2nd𝜔
↔ ∃𝑦 ∈
TopBases (𝑦 ≼ ω
∧ (topGen‘𝑦) =
𝐽)) |
39 | 37, 38 | sylibr 223 |
. . 3
⊢ ((𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽) → 𝐽 ∈
2nd𝜔) |
40 | 39 | exlimiv 1845 |
. 2
⊢
(∃𝑥(𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽) → 𝐽 ∈
2nd𝜔) |
41 | 23, 40 | impbii 198 |
1
⊢ (𝐽 ∈ 2nd𝜔
↔ ∃𝑥(𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽)) |