| Step | Hyp | Ref
| Expression |
| 1 | | df-lm 23237 |
. 2
⊢
⇝𝑡 = (𝑗 ∈ Top ↦ {〈𝑓, 𝑥〉 ∣ (𝑓 ∈ (∪ 𝑗 ↑pm ℂ)
∧ 𝑥 ∈ ∪ 𝑗
∧ ∀𝑢 ∈
𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))}) |
| 2 | | simpr 484 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → 𝑗 = 𝐽) |
| 3 | 2 | unieqd 4920 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → ∪ 𝑗 = ∪
𝐽) |
| 4 | | toponuni 22920 |
. . . . . . . 8
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
| 5 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → 𝑋 = ∪ 𝐽) |
| 6 | 3, 5 | eqtr4d 2780 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → ∪ 𝑗 = 𝑋) |
| 7 | 6 | oveq1d 7446 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → (∪ 𝑗 ↑pm ℂ) =
(𝑋 ↑pm
ℂ)) |
| 8 | 7 | eleq2d 2827 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → (𝑓 ∈ (∪ 𝑗 ↑pm ℂ)
↔ 𝑓 ∈ (𝑋 ↑pm
ℂ))) |
| 9 | 6 | eleq2d 2827 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → (𝑥 ∈ ∪ 𝑗 ↔ 𝑥 ∈ 𝑋)) |
| 10 | 2 | raleqdv 3326 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → (∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢) ↔ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))) |
| 11 | 8, 9, 10 | 3anbi123d 1438 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → ((𝑓 ∈ (∪ 𝑗 ↑pm ℂ)
∧ 𝑥 ∈ ∪ 𝑗
∧ ∀𝑢 ∈
𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢)) ↔ (𝑓 ∈ (𝑋 ↑pm ℂ) ∧ 𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢)))) |
| 12 | 11 | opabbidv 5209 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → {〈𝑓, 𝑥〉 ∣ (𝑓 ∈ (∪ 𝑗 ↑pm ℂ)
∧ 𝑥 ∈ ∪ 𝑗
∧ ∀𝑢 ∈
𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))} = {〈𝑓, 𝑥〉 ∣ (𝑓 ∈ (𝑋 ↑pm ℂ) ∧ 𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))}) |
| 13 | | topontop 22919 |
. 2
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
| 14 | | df-3an 1089 |
. . . . 5
⊢ ((𝑓 ∈ (𝑋 ↑pm ℂ) ∧ 𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢)) ↔ ((𝑓 ∈ (𝑋 ↑pm ℂ) ∧ 𝑥 ∈ 𝑋) ∧ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))) |
| 15 | 14 | opabbii 5210 |
. . . 4
⊢
{〈𝑓, 𝑥〉 ∣ (𝑓 ∈ (𝑋 ↑pm ℂ) ∧ 𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))} = {〈𝑓, 𝑥〉 ∣ ((𝑓 ∈ (𝑋 ↑pm ℂ) ∧ 𝑥 ∈ 𝑋) ∧ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))} |
| 16 | | opabssxp 5778 |
. . . 4
⊢
{〈𝑓, 𝑥〉 ∣ ((𝑓 ∈ (𝑋 ↑pm ℂ) ∧ 𝑥 ∈ 𝑋) ∧ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))} ⊆ ((𝑋 ↑pm ℂ) × 𝑋) |
| 17 | 15, 16 | eqsstri 4030 |
. . 3
⊢
{〈𝑓, 𝑥〉 ∣ (𝑓 ∈ (𝑋 ↑pm ℂ) ∧ 𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))} ⊆ ((𝑋 ↑pm ℂ) × 𝑋) |
| 18 | | ovex 7464 |
. . . 4
⊢ (𝑋 ↑pm ℂ)
∈ V |
| 19 | | toponmax 22932 |
. . . 4
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽) |
| 20 | | xpexg 7770 |
. . . 4
⊢ (((𝑋 ↑pm ℂ)
∈ V ∧ 𝑋 ∈
𝐽) → ((𝑋 ↑pm ℂ)
× 𝑋) ∈
V) |
| 21 | 18, 19, 20 | sylancr 587 |
. . 3
⊢ (𝐽 ∈ (TopOn‘𝑋) → ((𝑋 ↑pm ℂ) × 𝑋) ∈ V) |
| 22 | | ssexg 5323 |
. . 3
⊢
(({〈𝑓, 𝑥〉 ∣ (𝑓 ∈ (𝑋 ↑pm ℂ) ∧ 𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))} ⊆ ((𝑋 ↑pm ℂ) × 𝑋) ∧ ((𝑋 ↑pm ℂ) × 𝑋) ∈ V) → {〈𝑓, 𝑥〉 ∣ (𝑓 ∈ (𝑋 ↑pm ℂ) ∧ 𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))} ∈ V) |
| 23 | 17, 21, 22 | sylancr 587 |
. 2
⊢ (𝐽 ∈ (TopOn‘𝑋) → {〈𝑓, 𝑥〉 ∣ (𝑓 ∈ (𝑋 ↑pm ℂ) ∧ 𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))} ∈ V) |
| 24 | 1, 12, 13, 23 | fvmptd2 7024 |
1
⊢ (𝐽 ∈ (TopOn‘𝑋) →
(⇝𝑡‘𝐽) = {〈𝑓, 𝑥〉 ∣ (𝑓 ∈ (𝑋 ↑pm ℂ) ∧ 𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))}) |