Step |
Hyp |
Ref |
Expression |
1 |
|
qtopval.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
|
simp1 |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝐽 ∈ 𝑉 ) |
3 |
|
fof |
⊢ ( 𝐹 : 𝑍 –onto→ 𝑌 → 𝐹 : 𝑍 ⟶ 𝑌 ) |
4 |
3
|
3ad2ant2 |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝐹 : 𝑍 ⟶ 𝑌 ) |
5 |
|
uniexg |
⊢ ( 𝐽 ∈ 𝑉 → ∪ 𝐽 ∈ V ) |
6 |
5
|
3ad2ant1 |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ∪ 𝐽 ∈ V ) |
7 |
1 6
|
eqeltrid |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝑋 ∈ V ) |
8 |
|
simp3 |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝑍 ⊆ 𝑋 ) |
9 |
7 8
|
ssexd |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝑍 ∈ V ) |
10 |
|
fex |
⊢ ( ( 𝐹 : 𝑍 ⟶ 𝑌 ∧ 𝑍 ∈ V ) → 𝐹 ∈ V ) |
11 |
4 9 10
|
syl2anc |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝐹 ∈ V ) |
12 |
1
|
qtopval |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 ∈ V ) → ( 𝐽 qTop 𝐹 ) = { 𝑠 ∈ 𝒫 ( 𝐹 “ 𝑋 ) ∣ ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } ) |
13 |
2 11 12
|
syl2anc |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐽 qTop 𝐹 ) = { 𝑠 ∈ 𝒫 ( 𝐹 “ 𝑋 ) ∣ ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } ) |
14 |
|
imassrn |
⊢ ( 𝐹 “ 𝑋 ) ⊆ ran 𝐹 |
15 |
|
forn |
⊢ ( 𝐹 : 𝑍 –onto→ 𝑌 → ran 𝐹 = 𝑌 ) |
16 |
15
|
3ad2ant2 |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ran 𝐹 = 𝑌 ) |
17 |
14 16
|
sseqtrid |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐹 “ 𝑋 ) ⊆ 𝑌 ) |
18 |
|
foima |
⊢ ( 𝐹 : 𝑍 –onto→ 𝑌 → ( 𝐹 “ 𝑍 ) = 𝑌 ) |
19 |
18
|
3ad2ant2 |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐹 “ 𝑍 ) = 𝑌 ) |
20 |
|
imass2 |
⊢ ( 𝑍 ⊆ 𝑋 → ( 𝐹 “ 𝑍 ) ⊆ ( 𝐹 “ 𝑋 ) ) |
21 |
8 20
|
syl |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐹 “ 𝑍 ) ⊆ ( 𝐹 “ 𝑋 ) ) |
22 |
19 21
|
eqsstrrd |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝑌 ⊆ ( 𝐹 “ 𝑋 ) ) |
23 |
17 22
|
eqssd |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐹 “ 𝑋 ) = 𝑌 ) |
24 |
23
|
pweqd |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝒫 ( 𝐹 “ 𝑋 ) = 𝒫 𝑌 ) |
25 |
|
cnvimass |
⊢ ( ◡ 𝐹 “ 𝑠 ) ⊆ dom 𝐹 |
26 |
25 4
|
fssdm |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( ◡ 𝐹 “ 𝑠 ) ⊆ 𝑍 ) |
27 |
26 8
|
sstrd |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( ◡ 𝐹 “ 𝑠 ) ⊆ 𝑋 ) |
28 |
|
df-ss |
⊢ ( ( ◡ 𝐹 “ 𝑠 ) ⊆ 𝑋 ↔ ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) = ( ◡ 𝐹 “ 𝑠 ) ) |
29 |
27 28
|
sylib |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) = ( ◡ 𝐹 “ 𝑠 ) ) |
30 |
29
|
eleq1d |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 ↔ ( ◡ 𝐹 “ 𝑠 ) ∈ 𝐽 ) ) |
31 |
24 30
|
rabeqbidv |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → { 𝑠 ∈ 𝒫 ( 𝐹 “ 𝑋 ) ∣ ( ( ◡ 𝐹 “ 𝑠 ) ∩ 𝑋 ) ∈ 𝐽 } = { 𝑠 ∈ 𝒫 𝑌 ∣ ( ◡ 𝐹 “ 𝑠 ) ∈ 𝐽 } ) |
32 |
13 31
|
eqtrd |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐽 qTop 𝐹 ) = { 𝑠 ∈ 𝒫 𝑌 ∣ ( ◡ 𝐹 “ 𝑠 ) ∈ 𝐽 } ) |