Step | Hyp | Ref
| Expression |
1 | | is2ndc 21249 |
. . 3
⊢ (𝐽 ∈ 2nd𝜔
↔ ∃𝑥 ∈
TopBases (𝑥 ≼ ω
∧ (topGen‘𝑥) =
𝐽)) |
2 | | df-rex 2918 |
. . . 4
⊢
(∃𝑥 ∈
TopBases (𝑥 ≼ ω
∧ (topGen‘𝑥) =
𝐽) ↔ ∃𝑥(𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝐽))) |
3 | | simprl 794 |
. . . . . 6
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → 𝑥 ≼ ω) |
4 | | ssfii 8325 |
. . . . . . . . 9
⊢ (𝑥 ∈ TopBases → 𝑥 ⊆ (fi‘𝑥)) |
5 | 4 | adantr 481 |
. . . . . . . 8
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → 𝑥 ⊆ (fi‘𝑥)) |
6 | | fvex 6201 |
. . . . . . . . . 10
⊢
(topGen‘𝑥)
∈ V |
7 | | bastg 20770 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ TopBases → 𝑥 ⊆ (topGen‘𝑥)) |
8 | 7 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → 𝑥 ⊆ (topGen‘𝑥)) |
9 | | fiss 8330 |
. . . . . . . . . 10
⊢
(((topGen‘𝑥)
∈ V ∧ 𝑥 ⊆
(topGen‘𝑥)) →
(fi‘𝑥) ⊆
(fi‘(topGen‘𝑥))) |
10 | 6, 8, 9 | sylancr 695 |
. . . . . . . . 9
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → (fi‘𝑥) ⊆
(fi‘(topGen‘𝑥))) |
11 | | tgcl 20773 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ TopBases →
(topGen‘𝑥) ∈
Top) |
12 | 11 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → (topGen‘𝑥) ∈ Top) |
13 | | fitop 20705 |
. . . . . . . . . 10
⊢
((topGen‘𝑥)
∈ Top → (fi‘(topGen‘𝑥)) = (topGen‘𝑥)) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) →
(fi‘(topGen‘𝑥))
= (topGen‘𝑥)) |
15 | 10, 14 | sseqtrd 3641 |
. . . . . . . 8
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → (fi‘𝑥) ⊆ (topGen‘𝑥)) |
16 | | 2basgen 20794 |
. . . . . . . 8
⊢ ((𝑥 ⊆ (fi‘𝑥) ∧ (fi‘𝑥) ⊆ (topGen‘𝑥)) → (topGen‘𝑥) =
(topGen‘(fi‘𝑥))) |
17 | 5, 15, 16 | syl2anc 693 |
. . . . . . 7
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → (topGen‘𝑥) =
(topGen‘(fi‘𝑥))) |
18 | | simprr 796 |
. . . . . . 7
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → (topGen‘𝑥) = 𝐽) |
19 | 17, 18 | eqtr3d 2658 |
. . . . . 6
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) →
(topGen‘(fi‘𝑥))
= 𝐽) |
20 | 3, 19 | jca 554 |
. . . . 5
⊢ ((𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → (𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽)) |
21 | 20 | eximi 1762 |
. . . 4
⊢
(∃𝑥(𝑥 ∈ TopBases ∧ (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝐽)) → ∃𝑥(𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽)) |
22 | 2, 21 | sylbi 207 |
. . 3
⊢
(∃𝑥 ∈
TopBases (𝑥 ≼ ω
∧ (topGen‘𝑥) =
𝐽) → ∃𝑥(𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽)) |
23 | 1, 22 | sylbi 207 |
. 2
⊢ (𝐽 ∈ 2nd𝜔
→ ∃𝑥(𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽)) |
24 | | fibas 20781 |
. . . . 5
⊢
(fi‘𝑥) ∈
TopBases |
25 | | simpl 473 |
. . . . . . 7
⊢ ((𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽) → 𝑥 ≼
ω) |
26 | | vex 3203 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
27 | | fictb 9067 |
. . . . . . . 8
⊢ (𝑥 ∈ V → (𝑥 ≼ ω ↔
(fi‘𝑥) ≼
ω)) |
28 | 26, 27 | ax-mp 5 |
. . . . . . 7
⊢ (𝑥 ≼ ω ↔
(fi‘𝑥) ≼
ω) |
29 | 25, 28 | sylib 208 |
. . . . . 6
⊢ ((𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽) → (fi‘𝑥) ≼
ω) |
30 | | simpr 477 |
. . . . . 6
⊢ ((𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽) →
(topGen‘(fi‘𝑥))
= 𝐽) |
31 | 29, 30 | jca 554 |
. . . . 5
⊢ ((𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽) →
((fi‘𝑥) ≼
ω ∧ (topGen‘(fi‘𝑥)) = 𝐽)) |
32 | | breq1 4656 |
. . . . . . 7
⊢ (𝑦 = (fi‘𝑥) → (𝑦 ≼ ω ↔ (fi‘𝑥) ≼
ω)) |
33 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑦 = (fi‘𝑥) → (topGen‘𝑦) = (topGen‘(fi‘𝑥))) |
34 | 33 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑦 = (fi‘𝑥) → ((topGen‘𝑦) = 𝐽 ↔ (topGen‘(fi‘𝑥)) = 𝐽)) |
35 | 32, 34 | anbi12d 747 |
. . . . . 6
⊢ (𝑦 = (fi‘𝑥) → ((𝑦 ≼ ω ∧ (topGen‘𝑦) = 𝐽) ↔ ((fi‘𝑥) ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽))) |
36 | 35 | rspcev 3309 |
. . . . 5
⊢
(((fi‘𝑥)
∈ TopBases ∧ ((fi‘𝑥) ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽)) → ∃𝑦 ∈ TopBases (𝑦 ≼ ω ∧
(topGen‘𝑦) = 𝐽)) |
37 | 24, 31, 36 | sylancr 695 |
. . . 4
⊢ ((𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽) → ∃𝑦 ∈ TopBases (𝑦 ≼ ω ∧
(topGen‘𝑦) = 𝐽)) |
38 | | is2ndc 21249 |
. . . 4
⊢ (𝐽 ∈ 2nd𝜔
↔ ∃𝑦 ∈
TopBases (𝑦 ≼ ω
∧ (topGen‘𝑦) =
𝐽)) |
39 | 37, 38 | sylibr 224 |
. . 3
⊢ ((𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽) → 𝐽 ∈
2nd𝜔) |
40 | 39 | exlimiv 1858 |
. 2
⊢
(∃𝑥(𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽) → 𝐽 ∈
2nd𝜔) |
41 | 23, 40 | impbii 199 |
1
⊢ (𝐽 ∈ 2nd𝜔
↔ ∃𝑥(𝑥 ≼ ω ∧
(topGen‘(fi‘𝑥))
= 𝐽)) |