Step | Hyp | Ref
| Expression |
1 | | resima 5859 |
. . . . . . 7
⊢ ((𝐹 ↾ 𝑋) “ 𝑋) = (𝐹 “ 𝑋) |
2 | 1 | pweqi 4506 |
. . . . . 6
⊢ 𝒫
((𝐹 ↾ 𝑋) “ 𝑋) = 𝒫 (𝐹 “ 𝑋) |
3 | 2 | rabeqi 3383 |
. . . . 5
⊢ {𝑠 ∈ 𝒫 ((𝐹 ↾ 𝑋) “ 𝑋) ∣ ((◡(𝐹 ↾ 𝑋) “ 𝑠) ∩ 𝑋) ∈ 𝐽} = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡(𝐹 ↾ 𝑋) “ 𝑠) ∩ 𝑋) ∈ 𝐽} |
4 | | residm 5858 |
. . . . . . . . . 10
⊢ ((𝐹 ↾ 𝑋) ↾ 𝑋) = (𝐹 ↾ 𝑋) |
5 | 4 | cnveqi 5717 |
. . . . . . . . 9
⊢ ◡((𝐹 ↾ 𝑋) ↾ 𝑋) = ◡(𝐹 ↾ 𝑋) |
6 | 5 | imaeq1i 5900 |
. . . . . . . 8
⊢ (◡((𝐹 ↾ 𝑋) ↾ 𝑋) “ 𝑠) = (◡(𝐹 ↾ 𝑋) “ 𝑠) |
7 | | cnvresima 6062 |
. . . . . . . 8
⊢ (◡((𝐹 ↾ 𝑋) ↾ 𝑋) “ 𝑠) = ((◡(𝐹 ↾ 𝑋) “ 𝑠) ∩ 𝑋) |
8 | | cnvresima 6062 |
. . . . . . . 8
⊢ (◡(𝐹 ↾ 𝑋) “ 𝑠) = ((◡𝐹 “ 𝑠) ∩ 𝑋) |
9 | 6, 7, 8 | 3eqtr3i 2769 |
. . . . . . 7
⊢ ((◡(𝐹 ↾ 𝑋) “ 𝑠) ∩ 𝑋) = ((◡𝐹 “ 𝑠) ∩ 𝑋) |
10 | 9 | eleq1i 2823 |
. . . . . 6
⊢ (((◡(𝐹 ↾ 𝑋) “ 𝑠) ∩ 𝑋) ∈ 𝐽 ↔ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽) |
11 | 10 | rabbii 3374 |
. . . . 5
⊢ {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡(𝐹 ↾ 𝑋) “ 𝑠) ∩ 𝑋) ∈ 𝐽} = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽} |
12 | 3, 11 | eqtr2i 2762 |
. . . 4
⊢ {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽} = {𝑠 ∈ 𝒫 ((𝐹 ↾ 𝑋) “ 𝑋) ∣ ((◡(𝐹 ↾ 𝑋) “ 𝑠) ∩ 𝑋) ∈ 𝐽} |
13 | | qtopval.1 |
. . . . 5
⊢ 𝑋 = ∪
𝐽 |
14 | 13 | qtopval 22446 |
. . . 4
⊢ ((𝐽 ∈ V ∧ 𝐹 ∈ 𝑉) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |
15 | | resexg 5871 |
. . . . 5
⊢ (𝐹 ∈ 𝑉 → (𝐹 ↾ 𝑋) ∈ V) |
16 | 13 | qtopval 22446 |
. . . . 5
⊢ ((𝐽 ∈ V ∧ (𝐹 ↾ 𝑋) ∈ V) → (𝐽 qTop (𝐹 ↾ 𝑋)) = {𝑠 ∈ 𝒫 ((𝐹 ↾ 𝑋) “ 𝑋) ∣ ((◡(𝐹 ↾ 𝑋) “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |
17 | 15, 16 | sylan2 596 |
. . . 4
⊢ ((𝐽 ∈ V ∧ 𝐹 ∈ 𝑉) → (𝐽 qTop (𝐹 ↾ 𝑋)) = {𝑠 ∈ 𝒫 ((𝐹 ↾ 𝑋) “ 𝑋) ∣ ((◡(𝐹 ↾ 𝑋) “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |
18 | 12, 14, 17 | 3eqtr4a 2799 |
. . 3
⊢ ((𝐽 ∈ V ∧ 𝐹 ∈ 𝑉) → (𝐽 qTop 𝐹) = (𝐽 qTop (𝐹 ↾ 𝑋))) |
19 | 18 | expcom 417 |
. 2
⊢ (𝐹 ∈ 𝑉 → (𝐽 ∈ V → (𝐽 qTop 𝐹) = (𝐽 qTop (𝐹 ↾ 𝑋)))) |
20 | | df-qtop 16883 |
. . . . 5
⊢ qTop =
(𝑗 ∈ V, 𝑓 ∈ V ↦ {𝑠 ∈ 𝒫 (𝑓 “ ∪ 𝑗)
∣ ((◡𝑓 “ 𝑠) ∩ ∪ 𝑗) ∈ 𝑗}) |
21 | 20 | reldmmpo 7300 |
. . . 4
⊢ Rel dom
qTop |
22 | 21 | ovprc1 7209 |
. . 3
⊢ (¬
𝐽 ∈ V → (𝐽 qTop 𝐹) = ∅) |
23 | 21 | ovprc1 7209 |
. . 3
⊢ (¬
𝐽 ∈ V → (𝐽 qTop (𝐹 ↾ 𝑋)) = ∅) |
24 | 22, 23 | eqtr4d 2776 |
. 2
⊢ (¬
𝐽 ∈ V → (𝐽 qTop 𝐹) = (𝐽 qTop (𝐹 ↾ 𝑋))) |
25 | 19, 24 | pm2.61d1 183 |
1
⊢ (𝐹 ∈ 𝑉 → (𝐽 qTop 𝐹) = (𝐽 qTop (𝐹 ↾ 𝑋))) |