Step | Hyp | Ref
| Expression |
1 | | resima 5431 |
. . . . . . 7
⊢ ((𝐹 ↾ 𝑋) “ 𝑋) = (𝐹 “ 𝑋) |
2 | 1 | pweqi 4162 |
. . . . . 6
⊢ 𝒫
((𝐹 ↾ 𝑋) “ 𝑋) = 𝒫 (𝐹 “ 𝑋) |
3 | | rabeq 3192 |
. . . . . 6
⊢
(𝒫 ((𝐹
↾ 𝑋) “ 𝑋) = 𝒫 (𝐹 “ 𝑋) → {𝑠 ∈ 𝒫 ((𝐹 ↾ 𝑋) “ 𝑋) ∣ ((◡(𝐹 ↾ 𝑋) “ 𝑠) ∩ 𝑋) ∈ 𝐽} = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡(𝐹 ↾ 𝑋) “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |
4 | 2, 3 | ax-mp 5 |
. . . . 5
⊢ {𝑠 ∈ 𝒫 ((𝐹 ↾ 𝑋) “ 𝑋) ∣ ((◡(𝐹 ↾ 𝑋) “ 𝑠) ∩ 𝑋) ∈ 𝐽} = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡(𝐹 ↾ 𝑋) “ 𝑠) ∩ 𝑋) ∈ 𝐽} |
5 | | residm 5430 |
. . . . . . . . . . 11
⊢ ((𝐹 ↾ 𝑋) ↾ 𝑋) = (𝐹 ↾ 𝑋) |
6 | 5 | cnveqi 5297 |
. . . . . . . . . 10
⊢ ◡((𝐹 ↾ 𝑋) ↾ 𝑋) = ◡(𝐹 ↾ 𝑋) |
7 | 6 | imaeq1i 5463 |
. . . . . . . . 9
⊢ (◡((𝐹 ↾ 𝑋) ↾ 𝑋) “ 𝑠) = (◡(𝐹 ↾ 𝑋) “ 𝑠) |
8 | | cnvresima 5623 |
. . . . . . . . 9
⊢ (◡((𝐹 ↾ 𝑋) ↾ 𝑋) “ 𝑠) = ((◡(𝐹 ↾ 𝑋) “ 𝑠) ∩ 𝑋) |
9 | | cnvresima 5623 |
. . . . . . . . 9
⊢ (◡(𝐹 ↾ 𝑋) “ 𝑠) = ((◡𝐹 “ 𝑠) ∩ 𝑋) |
10 | 7, 8, 9 | 3eqtr3i 2652 |
. . . . . . . 8
⊢ ((◡(𝐹 ↾ 𝑋) “ 𝑠) ∩ 𝑋) = ((◡𝐹 “ 𝑠) ∩ 𝑋) |
11 | 10 | eleq1i 2692 |
. . . . . . 7
⊢ (((◡(𝐹 ↾ 𝑋) “ 𝑠) ∩ 𝑋) ∈ 𝐽 ↔ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽) |
12 | 11 | a1i 11 |
. . . . . 6
⊢ (𝑠 ∈ 𝒫 (𝐹 “ 𝑋) → (((◡(𝐹 ↾ 𝑋) “ 𝑠) ∩ 𝑋) ∈ 𝐽 ↔ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽)) |
13 | 12 | rabbiia 3185 |
. . . . 5
⊢ {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡(𝐹 ↾ 𝑋) “ 𝑠) ∩ 𝑋) ∈ 𝐽} = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽} |
14 | 4, 13 | eqtr2i 2645 |
. . . 4
⊢ {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽} = {𝑠 ∈ 𝒫 ((𝐹 ↾ 𝑋) “ 𝑋) ∣ ((◡(𝐹 ↾ 𝑋) “ 𝑠) ∩ 𝑋) ∈ 𝐽} |
15 | | qtopval.1 |
. . . . 5
⊢ 𝑋 = ∪
𝐽 |
16 | 15 | qtopval 21498 |
. . . 4
⊢ ((𝐽 ∈ V ∧ 𝐹 ∈ 𝑉) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |
17 | | resexg 5442 |
. . . . 5
⊢ (𝐹 ∈ 𝑉 → (𝐹 ↾ 𝑋) ∈ V) |
18 | 15 | qtopval 21498 |
. . . . 5
⊢ ((𝐽 ∈ V ∧ (𝐹 ↾ 𝑋) ∈ V) → (𝐽 qTop (𝐹 ↾ 𝑋)) = {𝑠 ∈ 𝒫 ((𝐹 ↾ 𝑋) “ 𝑋) ∣ ((◡(𝐹 ↾ 𝑋) “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |
19 | 17, 18 | sylan2 491 |
. . . 4
⊢ ((𝐽 ∈ V ∧ 𝐹 ∈ 𝑉) → (𝐽 qTop (𝐹 ↾ 𝑋)) = {𝑠 ∈ 𝒫 ((𝐹 ↾ 𝑋) “ 𝑋) ∣ ((◡(𝐹 ↾ 𝑋) “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |
20 | 14, 16, 19 | 3eqtr4a 2682 |
. . 3
⊢ ((𝐽 ∈ V ∧ 𝐹 ∈ 𝑉) → (𝐽 qTop 𝐹) = (𝐽 qTop (𝐹 ↾ 𝑋))) |
21 | 20 | expcom 451 |
. 2
⊢ (𝐹 ∈ 𝑉 → (𝐽 ∈ V → (𝐽 qTop 𝐹) = (𝐽 qTop (𝐹 ↾ 𝑋)))) |
22 | | df-qtop 16167 |
. . . . 5
⊢ qTop =
(𝑗 ∈ V, 𝑓 ∈ V ↦ {𝑠 ∈ 𝒫 (𝑓 “ ∪ 𝑗)
∣ ((◡𝑓 “ 𝑠) ∩ ∪ 𝑗) ∈ 𝑗}) |
23 | 22 | reldmmpt2 6771 |
. . . 4
⊢ Rel dom
qTop |
24 | 23 | ovprc1 6684 |
. . 3
⊢ (¬
𝐽 ∈ V → (𝐽 qTop 𝐹) = ∅) |
25 | 23 | ovprc1 6684 |
. . 3
⊢ (¬
𝐽 ∈ V → (𝐽 qTop (𝐹 ↾ 𝑋)) = ∅) |
26 | 24, 25 | eqtr4d 2659 |
. 2
⊢ (¬
𝐽 ∈ V → (𝐽 qTop 𝐹) = (𝐽 qTop (𝐹 ↾ 𝑋))) |
27 | 21, 26 | pm2.61d1 171 |
1
⊢ (𝐹 ∈ 𝑉 → (𝐽 qTop 𝐹) = (𝐽 qTop (𝐹 ↾ 𝑋))) |