Proof of Theorem qtopval2
Step | Hyp | Ref
| Expression |
1 | | simp1 1054 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝐽 ∈ 𝑉) |
2 | | fof 6028 |
. . . . 5
⊢ (𝐹:𝑍–onto→𝑌 → 𝐹:𝑍⟶𝑌) |
3 | 2 | 3ad2ant2 1076 |
. . . 4
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝐹:𝑍⟶𝑌) |
4 | | qtopval.1 |
. . . . . 6
⊢ 𝑋 = ∪
𝐽 |
5 | | uniexg 6853 |
. . . . . . 7
⊢ (𝐽 ∈ 𝑉 → ∪ 𝐽 ∈ V) |
6 | 5 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → ∪ 𝐽 ∈ V) |
7 | 4, 6 | syl5eqel 2692 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝑋 ∈ V) |
8 | | simp3 1056 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝑍 ⊆ 𝑋) |
9 | 7, 8 | ssexd 4733 |
. . . 4
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝑍 ∈ V) |
10 | | fex 6394 |
. . . 4
⊢ ((𝐹:𝑍⟶𝑌 ∧ 𝑍 ∈ V) → 𝐹 ∈ V) |
11 | 3, 9, 10 | syl2anc 691 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝐹 ∈ V) |
12 | 4 | qtopval 21308 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹 ∈ V) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |
13 | 1, 11, 12 | syl2anc 691 |
. 2
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽}) |
14 | | imassrn 5396 |
. . . . . 6
⊢ (𝐹 “ 𝑋) ⊆ ran 𝐹 |
15 | | forn 6031 |
. . . . . . 7
⊢ (𝐹:𝑍–onto→𝑌 → ran 𝐹 = 𝑌) |
16 | 15 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → ran 𝐹 = 𝑌) |
17 | 14, 16 | syl5sseq 3616 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐹 “ 𝑋) ⊆ 𝑌) |
18 | | foima 6033 |
. . . . . . 7
⊢ (𝐹:𝑍–onto→𝑌 → (𝐹 “ 𝑍) = 𝑌) |
19 | 18 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐹 “ 𝑍) = 𝑌) |
20 | | imass2 5420 |
. . . . . . 7
⊢ (𝑍 ⊆ 𝑋 → (𝐹 “ 𝑍) ⊆ (𝐹 “ 𝑋)) |
21 | 8, 20 | syl 17 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐹 “ 𝑍) ⊆ (𝐹 “ 𝑋)) |
22 | 19, 21 | eqsstr3d 3603 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝑌 ⊆ (𝐹 “ 𝑋)) |
23 | 17, 22 | eqssd 3585 |
. . . 4
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐹 “ 𝑋) = 𝑌) |
24 | 23 | pweqd 4113 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → 𝒫 (𝐹 “ 𝑋) = 𝒫 𝑌) |
25 | | cnvimass 5404 |
. . . . . . 7
⊢ (◡𝐹 “ 𝑠) ⊆ dom 𝐹 |
26 | | fdm 5964 |
. . . . . . . 8
⊢ (𝐹:𝑍⟶𝑌 → dom 𝐹 = 𝑍) |
27 | 3, 26 | syl 17 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → dom 𝐹 = 𝑍) |
28 | 25, 27 | syl5sseq 3616 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (◡𝐹 “ 𝑠) ⊆ 𝑍) |
29 | 28, 8 | sstrd 3578 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (◡𝐹 “ 𝑠) ⊆ 𝑋) |
30 | | df-ss 3554 |
. . . . 5
⊢ ((◡𝐹 “ 𝑠) ⊆ 𝑋 ↔ ((◡𝐹 “ 𝑠) ∩ 𝑋) = (◡𝐹 “ 𝑠)) |
31 | 29, 30 | sylib 207 |
. . . 4
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → ((◡𝐹 “ 𝑠) ∩ 𝑋) = (◡𝐹 “ 𝑠)) |
32 | 31 | eleq1d 2672 |
. . 3
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽 ↔ (◡𝐹 “ 𝑠) ∈ 𝐽)) |
33 | 24, 32 | rabeqbidv 3168 |
. 2
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽} = {𝑠 ∈ 𝒫 𝑌 ∣ (◡𝐹 “ 𝑠) ∈ 𝐽}) |
34 | 13, 33 | eqtrd 2644 |
1
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 𝑌 ∣ (◡𝐹 “ 𝑠) ∈ 𝐽}) |