Proof of Theorem qtopval2
Step | Hyp | Ref
| Expression |
1 | | simp1 1132 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝐽 ∈ 𝑉) |
2 | | fof 6592 |
. . . . 5
⊢ (𝐹:𝑍–onto→𝑌 → 𝐹:𝑍⟶𝑌) |
3 | 2 | 3ad2ant2 1130 |
. . . 4
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝐹:𝑍⟶𝑌) |
4 | | qtopval.1 |
. . . . . 6
⊢ 𝑋 = ∪
𝐽 |
5 | | uniexg 7468 |
. . . . . . 7
⊢ (𝐽 ∈ 𝑉 → ∪ 𝐽 ∈ V) |
6 | 5 | 3ad2ant1 1129 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → ∪ 𝐽 ∈ V) |
7 | 4, 6 | eqeltrid 2919 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝑋 ∈ V) |
8 | | simp3 1134 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝑍 ⊆ 𝑋) |
9 | 7, 8 | ssexd 5230 |
. . . 4
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝑍 ∈ V) |
10 | | fex 6991 |
. . . 4
⊢ ((𝐹:𝑍⟶𝑌 ∧ 𝑍 ∈ V) → 𝐹 ∈ V) |
11 | 3, 9, 10 | syl2anc 586 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝐹 ∈ V) |
12 | 4 | qtopval 22305 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹 ∈ V) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |
13 | 1, 11, 12 | syl2anc 586 |
. 2
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |
14 | | imassrn 5942 |
. . . . . 6
⊢ (𝐹 “ 𝑋) ⊆ ran 𝐹 |
15 | | forn 6595 |
. . . . . . 7
⊢ (𝐹:𝑍–onto→𝑌 → ran 𝐹 = 𝑌) |
16 | 15 | 3ad2ant2 1130 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → ran 𝐹 = 𝑌) |
17 | 14, 16 | sseqtrid 4021 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐹 “ 𝑋) ⊆ 𝑌) |
18 | | foima 6597 |
. . . . . . 7
⊢ (𝐹:𝑍–onto→𝑌 → (𝐹 “ 𝑍) = 𝑌) |
19 | 18 | 3ad2ant2 1130 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐹 “ 𝑍) = 𝑌) |
20 | | imass2 5967 |
. . . . . . 7
⊢ (𝑍 ⊆ 𝑋 → (𝐹 “ 𝑍) ⊆ (𝐹 “ 𝑋)) |
21 | 8, 20 | syl 17 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐹 “ 𝑍) ⊆ (𝐹 “ 𝑋)) |
22 | 19, 21 | eqsstrrd 4008 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝑌 ⊆ (𝐹 “ 𝑋)) |
23 | 17, 22 | eqssd 3986 |
. . . 4
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐹 “ 𝑋) = 𝑌) |
24 | 23 | pweqd 4560 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝒫 (𝐹 “ 𝑋) = 𝒫 𝑌) |
25 | | cnvimass 5951 |
. . . . . . 7
⊢ (◡𝐹 “ 𝑠) ⊆ dom 𝐹 |
26 | 25, 3 | fssdm 6532 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (◡𝐹 “ 𝑠) ⊆ 𝑍) |
27 | 26, 8 | sstrd 3979 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (◡𝐹 “ 𝑠) ⊆ 𝑋) |
28 | | df-ss 3954 |
. . . . 5
⊢ ((◡𝐹 “ 𝑠) ⊆ 𝑋 ↔ ((◡𝐹 “ 𝑠) ∩ 𝑋) = (◡𝐹 “ 𝑠)) |
29 | 27, 28 | sylib 220 |
. . . 4
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → ((◡𝐹 “ 𝑠) ∩ 𝑋) = (◡𝐹 “ 𝑠)) |
30 | 29 | eleq1d 2899 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽 ↔ (◡𝐹 “ 𝑠) ∈ 𝐽)) |
31 | 24, 30 | rabeqbidv 3487 |
. 2
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽} = {𝑠 ∈ 𝒫 𝑌 ∣ (◡𝐹 “ 𝑠) ∈ 𝐽}) |
32 | 13, 31 | eqtrd 2858 |
1
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 𝑌 ∣ (◡𝐹 “ 𝑠) ∈ 𝐽}) |