| Step | Hyp | Ref
| Expression |
| 1 | | elex 3501 |
. 2
⊢ (𝐽 ∈ 𝑉 → 𝐽 ∈ V) |
| 2 | | elex 3501 |
. 2
⊢ (𝐹 ∈ 𝑊 → 𝐹 ∈ V) |
| 3 | | imaexg 7935 |
. . . . 5
⊢ (𝐹 ∈ V → (𝐹 “ 𝑋) ∈ V) |
| 4 | | pwexg 5378 |
. . . . 5
⊢ ((𝐹 “ 𝑋) ∈ V → 𝒫 (𝐹 “ 𝑋) ∈ V) |
| 5 | | rabexg 5337 |
. . . . 5
⊢
(𝒫 (𝐹
“ 𝑋) ∈ V →
{𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽} ∈ V) |
| 6 | 3, 4, 5 | 3syl 18 |
. . . 4
⊢ (𝐹 ∈ V → {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽} ∈ V) |
| 7 | 6 | adantl 481 |
. . 3
⊢ ((𝐽 ∈ V ∧ 𝐹 ∈ V) → {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽} ∈ V) |
| 8 | | simpr 484 |
. . . . . . 7
⊢ ((𝑗 = 𝐽 ∧ 𝑓 = 𝐹) → 𝑓 = 𝐹) |
| 9 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝑗 = 𝐽 ∧ 𝑓 = 𝐹) → 𝑗 = 𝐽) |
| 10 | 9 | unieqd 4920 |
. . . . . . . 8
⊢ ((𝑗 = 𝐽 ∧ 𝑓 = 𝐹) → ∪ 𝑗 = ∪
𝐽) |
| 11 | | qtopval.1 |
. . . . . . . 8
⊢ 𝑋 = ∪
𝐽 |
| 12 | 10, 11 | eqtr4di 2795 |
. . . . . . 7
⊢ ((𝑗 = 𝐽 ∧ 𝑓 = 𝐹) → ∪ 𝑗 = 𝑋) |
| 13 | 8, 12 | imaeq12d 6079 |
. . . . . 6
⊢ ((𝑗 = 𝐽 ∧ 𝑓 = 𝐹) → (𝑓 “ ∪ 𝑗) = (𝐹 “ 𝑋)) |
| 14 | 13 | pweqd 4617 |
. . . . 5
⊢ ((𝑗 = 𝐽 ∧ 𝑓 = 𝐹) → 𝒫 (𝑓 “ ∪ 𝑗) = 𝒫 (𝐹 “ 𝑋)) |
| 15 | 8 | cnveqd 5886 |
. . . . . . . 8
⊢ ((𝑗 = 𝐽 ∧ 𝑓 = 𝐹) → ◡𝑓 = ◡𝐹) |
| 16 | 15 | imaeq1d 6077 |
. . . . . . 7
⊢ ((𝑗 = 𝐽 ∧ 𝑓 = 𝐹) → (◡𝑓 “ 𝑠) = (◡𝐹 “ 𝑠)) |
| 17 | 16, 12 | ineq12d 4221 |
. . . . . 6
⊢ ((𝑗 = 𝐽 ∧ 𝑓 = 𝐹) → ((◡𝑓 “ 𝑠) ∩ ∪ 𝑗) = ((◡𝐹 “ 𝑠) ∩ 𝑋)) |
| 18 | 17, 9 | eleq12d 2835 |
. . . . 5
⊢ ((𝑗 = 𝐽 ∧ 𝑓 = 𝐹) → (((◡𝑓 “ 𝑠) ∩ ∪ 𝑗) ∈ 𝑗 ↔ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽)) |
| 19 | 14, 18 | rabeqbidv 3455 |
. . . 4
⊢ ((𝑗 = 𝐽 ∧ 𝑓 = 𝐹) → {𝑠 ∈ 𝒫 (𝑓 “ ∪ 𝑗) ∣ ((◡𝑓 “ 𝑠) ∩ ∪ 𝑗) ∈ 𝑗} = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |
| 20 | | df-qtop 17552 |
. . . 4
⊢ qTop =
(𝑗 ∈ V, 𝑓 ∈ V ↦ {𝑠 ∈ 𝒫 (𝑓 “ ∪ 𝑗)
∣ ((◡𝑓 “ 𝑠) ∩ ∪ 𝑗) ∈ 𝑗}) |
| 21 | 19, 20 | ovmpoga 7587 |
. . 3
⊢ ((𝐽 ∈ V ∧ 𝐹 ∈ V ∧ {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽} ∈ V) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |
| 22 | 7, 21 | mpd3an3 1464 |
. 2
⊢ ((𝐽 ∈ V ∧ 𝐹 ∈ V) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |
| 23 | 1, 2, 22 | syl2an 596 |
1
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |