Proof of Theorem qtopval2
Step | Hyp | Ref
| Expression |
1 | | simp1 1061 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝐽 ∈ 𝑉) |
2 | | fof 6115 |
. . . . 5
⊢ (𝐹:𝑍–onto→𝑌 → 𝐹:𝑍⟶𝑌) |
3 | 2 | 3ad2ant2 1083 |
. . . 4
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝐹:𝑍⟶𝑌) |
4 | | qtopval.1 |
. . . . . 6
⊢ 𝑋 = ∪
𝐽 |
5 | | uniexg 6955 |
. . . . . . 7
⊢ (𝐽 ∈ 𝑉 → ∪ 𝐽 ∈ V) |
6 | 5 | 3ad2ant1 1082 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → ∪ 𝐽 ∈ V) |
7 | 4, 6 | syl5eqel 2705 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝑋 ∈ V) |
8 | | simp3 1063 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝑍 ⊆ 𝑋) |
9 | 7, 8 | ssexd 4805 |
. . . 4
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝑍 ∈ V) |
10 | | fex 6490 |
. . . 4
⊢ ((𝐹:𝑍⟶𝑌 ∧ 𝑍 ∈ V) → 𝐹 ∈ V) |
11 | 3, 9, 10 | syl2anc 693 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝐹 ∈ V) |
12 | 4 | qtopval 21498 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹 ∈ V) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |
13 | 1, 11, 12 | syl2anc 693 |
. 2
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |
14 | | imassrn 5477 |
. . . . . 6
⊢ (𝐹 “ 𝑋) ⊆ ran 𝐹 |
15 | | forn 6118 |
. . . . . . 7
⊢ (𝐹:𝑍–onto→𝑌 → ran 𝐹 = 𝑌) |
16 | 15 | 3ad2ant2 1083 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → ran 𝐹 = 𝑌) |
17 | 14, 16 | syl5sseq 3653 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐹 “ 𝑋) ⊆ 𝑌) |
18 | | foima 6120 |
. . . . . . 7
⊢ (𝐹:𝑍–onto→𝑌 → (𝐹 “ 𝑍) = 𝑌) |
19 | 18 | 3ad2ant2 1083 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐹 “ 𝑍) = 𝑌) |
20 | | imass2 5501 |
. . . . . . 7
⊢ (𝑍 ⊆ 𝑋 → (𝐹 “ 𝑍) ⊆ (𝐹 “ 𝑋)) |
21 | 8, 20 | syl 17 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐹 “ 𝑍) ⊆ (𝐹 “ 𝑋)) |
22 | 19, 21 | eqsstr3d 3640 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝑌 ⊆ (𝐹 “ 𝑋)) |
23 | 17, 22 | eqssd 3620 |
. . . 4
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐹 “ 𝑋) = 𝑌) |
24 | 23 | pweqd 4163 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝒫 (𝐹 “ 𝑋) = 𝒫 𝑌) |
25 | | cnvimass 5485 |
. . . . . . 7
⊢ (◡𝐹 “ 𝑠) ⊆ dom 𝐹 |
26 | | fdm 6051 |
. . . . . . . 8
⊢ (𝐹:𝑍⟶𝑌 → dom 𝐹 = 𝑍) |
27 | 3, 26 | syl 17 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → dom 𝐹 = 𝑍) |
28 | 25, 27 | syl5sseq 3653 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (◡𝐹 “ 𝑠) ⊆ 𝑍) |
29 | 28, 8 | sstrd 3613 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (◡𝐹 “ 𝑠) ⊆ 𝑋) |
30 | | df-ss 3588 |
. . . . 5
⊢ ((◡𝐹 “ 𝑠) ⊆ 𝑋 ↔ ((◡𝐹 “ 𝑠) ∩ 𝑋) = (◡𝐹 “ 𝑠)) |
31 | 29, 30 | sylib 208 |
. . . 4
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → ((◡𝐹 “ 𝑠) ∩ 𝑋) = (◡𝐹 “ 𝑠)) |
32 | 31 | eleq1d 2686 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽 ↔ (◡𝐹 “ 𝑠) ∈ 𝐽)) |
33 | 24, 32 | rabeqbidv 3195 |
. 2
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽} = {𝑠 ∈ 𝒫 𝑌 ∣ (◡𝐹 “ 𝑠) ∈ 𝐽}) |
34 | 13, 33 | eqtrd 2656 |
1
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 𝑌 ∣ (◡𝐹 “ 𝑠) ∈ 𝐽}) |