Step | Hyp | Ref
| Expression |
1 | | df-kgen 21337 |
. . 3
⊢
𝑘Gen = (𝑗
∈ Top ↦ {𝑥
∈ 𝒫 ∪ 𝑗 ∣ ∀𝑘 ∈ 𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))}) |
2 | 1 | a1i 11 |
. 2
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑘Gen = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 ∪ 𝑗
∣ ∀𝑘 ∈
𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))})) |
3 | | unieq 4444 |
. . . . 5
⊢ (𝑗 = 𝐽 → ∪ 𝑗 = ∪
𝐽) |
4 | | toponuni 20719 |
. . . . . 6
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
5 | 4 | eqcomd 2628 |
. . . . 5
⊢ (𝐽 ∈ (TopOn‘𝑋) → ∪ 𝐽 =
𝑋) |
6 | 3, 5 | sylan9eqr 2678 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → ∪ 𝑗 = 𝑋) |
7 | 6 | pweqd 4163 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → 𝒫 ∪ 𝑗 =
𝒫 𝑋) |
8 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑗 = 𝐽 → (𝑗 ↾t 𝑘) = (𝐽 ↾t 𝑘)) |
9 | 8 | eleq1d 2686 |
. . . . . 6
⊢ (𝑗 = 𝐽 → ((𝑗 ↾t 𝑘) ∈ Comp ↔ (𝐽 ↾t 𝑘) ∈ Comp)) |
10 | 8 | eleq2d 2687 |
. . . . . 6
⊢ (𝑗 = 𝐽 → ((𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘) ↔ (𝑥 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))) |
11 | 9, 10 | imbi12d 334 |
. . . . 5
⊢ (𝑗 = 𝐽 → (((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘)) ↔ ((𝐽 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘)))) |
12 | 11 | adantl 482 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → (((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘)) ↔ ((𝐽 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘)))) |
13 | 7, 12 | raleqbidv 3152 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → (∀𝑘 ∈ 𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘)) ↔ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘)))) |
14 | 7, 13 | rabeqbidv 3195 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → {𝑥 ∈ 𝒫 ∪ 𝑗
∣ ∀𝑘 ∈
𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))} = {𝑥 ∈ 𝒫 𝑋 ∣ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))}) |
15 | | topontop 20718 |
. 2
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
16 | | toponmax 20730 |
. . 3
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽) |
17 | | pwexg 4850 |
. . 3
⊢ (𝑋 ∈ 𝐽 → 𝒫 𝑋 ∈ V) |
18 | | rabexg 4812 |
. . 3
⊢
(𝒫 𝑋 ∈
V → {𝑥 ∈
𝒫 𝑋 ∣
∀𝑘 ∈ 𝒫
𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))} ∈ V) |
19 | 16, 17, 18 | 3syl 18 |
. 2
⊢ (𝐽 ∈ (TopOn‘𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))} ∈ V) |
20 | 2, 14, 15, 19 | fvmptd 6288 |
1
⊢ (𝐽 ∈ (TopOn‘𝑋) →
(𝑘Gen‘𝐽) =
{𝑥 ∈ 𝒫 𝑋 ∣ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))}) |