Step | Hyp | Ref
| Expression |
1 | | elex 3426 |
. 2
⊢ (𝐽 ∈ 𝑉 → 𝐽 ∈ V) |
2 | | elex 3426 |
. 2
⊢ (𝐹 ∈ 𝑊 → 𝐹 ∈ V) |
3 | | imaexg 7693 |
. . . . 5
⊢ (𝐹 ∈ V → (𝐹 “ 𝑋) ∈ V) |
4 | | pwexg 5271 |
. . . . 5
⊢ ((𝐹 “ 𝑋) ∈ V → 𝒫 (𝐹 “ 𝑋) ∈ V) |
5 | | rabexg 5224 |
. . . . 5
⊢
(𝒫 (𝐹
“ 𝑋) ∈ V →
{𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽} ∈ V) |
6 | 3, 4, 5 | 3syl 18 |
. . . 4
⊢ (𝐹 ∈ V → {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽} ∈ V) |
7 | 6 | adantl 485 |
. . 3
⊢ ((𝐽 ∈ V ∧ 𝐹 ∈ V) → {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽} ∈ V) |
8 | | simpr 488 |
. . . . . . 7
⊢ ((𝑗 = 𝐽 ∧ 𝑓 = 𝐹) → 𝑓 = 𝐹) |
9 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝑗 = 𝐽 ∧ 𝑓 = 𝐹) → 𝑗 = 𝐽) |
10 | 9 | unieqd 4833 |
. . . . . . . 8
⊢ ((𝑗 = 𝐽 ∧ 𝑓 = 𝐹) → ∪ 𝑗 = ∪
𝐽) |
11 | | qtopval.1 |
. . . . . . . 8
⊢ 𝑋 = ∪
𝐽 |
12 | 10, 11 | eqtr4di 2796 |
. . . . . . 7
⊢ ((𝑗 = 𝐽 ∧ 𝑓 = 𝐹) → ∪ 𝑗 = 𝑋) |
13 | 8, 12 | imaeq12d 5930 |
. . . . . 6
⊢ ((𝑗 = 𝐽 ∧ 𝑓 = 𝐹) → (𝑓 “ ∪ 𝑗) = (𝐹 “ 𝑋)) |
14 | 13 | pweqd 4532 |
. . . . 5
⊢ ((𝑗 = 𝐽 ∧ 𝑓 = 𝐹) → 𝒫 (𝑓 “ ∪ 𝑗) = 𝒫 (𝐹 “ 𝑋)) |
15 | 8 | cnveqd 5744 |
. . . . . . . 8
⊢ ((𝑗 = 𝐽 ∧ 𝑓 = 𝐹) → ◡𝑓 = ◡𝐹) |
16 | 15 | imaeq1d 5928 |
. . . . . . 7
⊢ ((𝑗 = 𝐽 ∧ 𝑓 = 𝐹) → (◡𝑓 “ 𝑠) = (◡𝐹 “ 𝑠)) |
17 | 16, 12 | ineq12d 4128 |
. . . . . 6
⊢ ((𝑗 = 𝐽 ∧ 𝑓 = 𝐹) → ((◡𝑓 “ 𝑠) ∩ ∪ 𝑗) = ((◡𝐹 “ 𝑠) ∩ 𝑋)) |
18 | 17, 9 | eleq12d 2832 |
. . . . 5
⊢ ((𝑗 = 𝐽 ∧ 𝑓 = 𝐹) → (((◡𝑓 “ 𝑠) ∩ ∪ 𝑗) ∈ 𝑗 ↔ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽)) |
19 | 14, 18 | rabeqbidv 3396 |
. . . 4
⊢ ((𝑗 = 𝐽 ∧ 𝑓 = 𝐹) → {𝑠 ∈ 𝒫 (𝑓 “ ∪ 𝑗) ∣ ((◡𝑓 “ 𝑠) ∩ ∪ 𝑗) ∈ 𝑗} = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |
20 | | df-qtop 17012 |
. . . 4
⊢ qTop =
(𝑗 ∈ V, 𝑓 ∈ V ↦ {𝑠 ∈ 𝒫 (𝑓 “ ∪ 𝑗)
∣ ((◡𝑓 “ 𝑠) ∩ ∪ 𝑗) ∈ 𝑗}) |
21 | 19, 20 | ovmpoga 7363 |
. . 3
⊢ ((𝐽 ∈ V ∧ 𝐹 ∈ V ∧ {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽} ∈ V) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |
22 | 7, 21 | mpd3an3 1464 |
. 2
⊢ ((𝐽 ∈ V ∧ 𝐹 ∈ V) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |
23 | 1, 2, 22 | syl2an 599 |
1
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |