Proof of Theorem qtopval2
| Step | Hyp | Ref
| Expression |
| 1 | | simp1 1137 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝐽 ∈ 𝑉) |
| 2 | | fof 6820 |
. . . . 5
⊢ (𝐹:𝑍–onto→𝑌 → 𝐹:𝑍⟶𝑌) |
| 3 | 2 | 3ad2ant2 1135 |
. . . 4
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝐹:𝑍⟶𝑌) |
| 4 | | qtopval.1 |
. . . . . 6
⊢ 𝑋 = ∪
𝐽 |
| 5 | | uniexg 7760 |
. . . . . . 7
⊢ (𝐽 ∈ 𝑉 → ∪ 𝐽 ∈ V) |
| 6 | 5 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → ∪ 𝐽 ∈ V) |
| 7 | 4, 6 | eqeltrid 2845 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝑋 ∈ V) |
| 8 | | simp3 1139 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝑍 ⊆ 𝑋) |
| 9 | 7, 8 | ssexd 5324 |
. . . 4
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝑍 ∈ V) |
| 10 | 3, 9 | fexd 7247 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝐹 ∈ V) |
| 11 | 4 | qtopval 23703 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹 ∈ V) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |
| 12 | 1, 10, 11 | syl2anc 584 |
. 2
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |
| 13 | | imassrn 6089 |
. . . . . 6
⊢ (𝐹 “ 𝑋) ⊆ ran 𝐹 |
| 14 | | forn 6823 |
. . . . . . 7
⊢ (𝐹:𝑍–onto→𝑌 → ran 𝐹 = 𝑌) |
| 15 | 14 | 3ad2ant2 1135 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → ran 𝐹 = 𝑌) |
| 16 | 13, 15 | sseqtrid 4026 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐹 “ 𝑋) ⊆ 𝑌) |
| 17 | | foima 6825 |
. . . . . . 7
⊢ (𝐹:𝑍–onto→𝑌 → (𝐹 “ 𝑍) = 𝑌) |
| 18 | 17 | 3ad2ant2 1135 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐹 “ 𝑍) = 𝑌) |
| 19 | | imass2 6120 |
. . . . . . 7
⊢ (𝑍 ⊆ 𝑋 → (𝐹 “ 𝑍) ⊆ (𝐹 “ 𝑋)) |
| 20 | 8, 19 | syl 17 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐹 “ 𝑍) ⊆ (𝐹 “ 𝑋)) |
| 21 | 18, 20 | eqsstrrd 4019 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝑌 ⊆ (𝐹 “ 𝑋)) |
| 22 | 16, 21 | eqssd 4001 |
. . . 4
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐹 “ 𝑋) = 𝑌) |
| 23 | 22 | pweqd 4617 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝒫 (𝐹 “ 𝑋) = 𝒫 𝑌) |
| 24 | | cnvimass 6100 |
. . . . . . 7
⊢ (◡𝐹 “ 𝑠) ⊆ dom 𝐹 |
| 25 | 24, 3 | fssdm 6755 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (◡𝐹 “ 𝑠) ⊆ 𝑍) |
| 26 | 25, 8 | sstrd 3994 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (◡𝐹 “ 𝑠) ⊆ 𝑋) |
| 27 | | dfss2 3969 |
. . . . 5
⊢ ((◡𝐹 “ 𝑠) ⊆ 𝑋 ↔ ((◡𝐹 “ 𝑠) ∩ 𝑋) = (◡𝐹 “ 𝑠)) |
| 28 | 26, 27 | sylib 218 |
. . . 4
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → ((◡𝐹 “ 𝑠) ∩ 𝑋) = (◡𝐹 “ 𝑠)) |
| 29 | 28 | eleq1d 2826 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽 ↔ (◡𝐹 “ 𝑠) ∈ 𝐽)) |
| 30 | 23, 29 | rabeqbidv 3455 |
. 2
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽} = {𝑠 ∈ 𝒫 𝑌 ∣ (◡𝐹 “ 𝑠) ∈ 𝐽}) |
| 31 | 12, 30 | eqtrd 2777 |
1
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 𝑌 ∣ (◡𝐹 “ 𝑠) ∈ 𝐽}) |