Proof of Theorem qtopval2
Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝐽 ∈ 𝑉) |
2 | | fof 6593 |
. . . . 5
⊢ (𝐹:𝑍–onto→𝑌 → 𝐹:𝑍⟶𝑌) |
3 | 2 | 3ad2ant2 1135 |
. . . 4
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝐹:𝑍⟶𝑌) |
4 | | qtopval.1 |
. . . . . 6
⊢ 𝑋 = ∪
𝐽 |
5 | | uniexg 7487 |
. . . . . . 7
⊢ (𝐽 ∈ 𝑉 → ∪ 𝐽 ∈ V) |
6 | 5 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → ∪ 𝐽 ∈ V) |
7 | 4, 6 | eqeltrid 2838 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝑋 ∈ V) |
8 | | simp3 1139 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝑍 ⊆ 𝑋) |
9 | 7, 8 | ssexd 5193 |
. . . 4
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝑍 ∈ V) |
10 | 3, 9 | fexd 7003 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝐹 ∈ V) |
11 | 4 | qtopval 22449 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹 ∈ V) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |
12 | 1, 10, 11 | syl2anc 587 |
. 2
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |
13 | | imassrn 5915 |
. . . . . 6
⊢ (𝐹 “ 𝑋) ⊆ ran 𝐹 |
14 | | forn 6596 |
. . . . . . 7
⊢ (𝐹:𝑍–onto→𝑌 → ran 𝐹 = 𝑌) |
15 | 14 | 3ad2ant2 1135 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → ran 𝐹 = 𝑌) |
16 | 13, 15 | sseqtrid 3930 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐹 “ 𝑋) ⊆ 𝑌) |
17 | | foima 6598 |
. . . . . . 7
⊢ (𝐹:𝑍–onto→𝑌 → (𝐹 “ 𝑍) = 𝑌) |
18 | 17 | 3ad2ant2 1135 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐹 “ 𝑍) = 𝑌) |
19 | | imass2 5940 |
. . . . . . 7
⊢ (𝑍 ⊆ 𝑋 → (𝐹 “ 𝑍) ⊆ (𝐹 “ 𝑋)) |
20 | 8, 19 | syl 17 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐹 “ 𝑍) ⊆ (𝐹 “ 𝑋)) |
21 | 18, 20 | eqsstrrd 3917 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝑌 ⊆ (𝐹 “ 𝑋)) |
22 | 16, 21 | eqssd 3895 |
. . . 4
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐹 “ 𝑋) = 𝑌) |
23 | 22 | pweqd 4508 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝒫 (𝐹 “ 𝑋) = 𝒫 𝑌) |
24 | | cnvimass 5924 |
. . . . . . 7
⊢ (◡𝐹 “ 𝑠) ⊆ dom 𝐹 |
25 | 24, 3 | fssdm 6525 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (◡𝐹 “ 𝑠) ⊆ 𝑍) |
26 | 25, 8 | sstrd 3888 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (◡𝐹 “ 𝑠) ⊆ 𝑋) |
27 | | df-ss 3861 |
. . . . 5
⊢ ((◡𝐹 “ 𝑠) ⊆ 𝑋 ↔ ((◡𝐹 “ 𝑠) ∩ 𝑋) = (◡𝐹 “ 𝑠)) |
28 | 26, 27 | sylib 221 |
. . . 4
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → ((◡𝐹 “ 𝑠) ∩ 𝑋) = (◡𝐹 “ 𝑠)) |
29 | 28 | eleq1d 2818 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽 ↔ (◡𝐹 “ 𝑠) ∈ 𝐽)) |
30 | 23, 29 | rabeqbidv 3388 |
. 2
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽} = {𝑠 ∈ 𝒫 𝑌 ∣ (◡𝐹 “ 𝑠) ∈ 𝐽}) |
31 | 12, 30 | eqtrd 2774 |
1
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 𝑌 ∣ (◡𝐹 “ 𝑠) ∈ 𝐽}) |