Step |
Hyp |
Ref |
Expression |
1 |
|
qtopval.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
1
|
qtopval2 |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐽 qTop 𝐹 ) = { 𝑠 ∈ 𝒫 𝑌 ∣ ( ◡ 𝐹 “ 𝑠 ) ∈ 𝐽 } ) |
3 |
2
|
eleq2d |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐴 ∈ ( 𝐽 qTop 𝐹 ) ↔ 𝐴 ∈ { 𝑠 ∈ 𝒫 𝑌 ∣ ( ◡ 𝐹 “ 𝑠 ) ∈ 𝐽 } ) ) |
4 |
|
imaeq2 |
⊢ ( 𝑠 = 𝐴 → ( ◡ 𝐹 “ 𝑠 ) = ( ◡ 𝐹 “ 𝐴 ) ) |
5 |
4
|
eleq1d |
⊢ ( 𝑠 = 𝐴 → ( ( ◡ 𝐹 “ 𝑠 ) ∈ 𝐽 ↔ ( ◡ 𝐹 “ 𝐴 ) ∈ 𝐽 ) ) |
6 |
5
|
elrab |
⊢ ( 𝐴 ∈ { 𝑠 ∈ 𝒫 𝑌 ∣ ( ◡ 𝐹 “ 𝑠 ) ∈ 𝐽 } ↔ ( 𝐴 ∈ 𝒫 𝑌 ∧ ( ◡ 𝐹 “ 𝐴 ) ∈ 𝐽 ) ) |
7 |
|
uniexg |
⊢ ( 𝐽 ∈ 𝑉 → ∪ 𝐽 ∈ V ) |
8 |
1 7
|
eqeltrid |
⊢ ( 𝐽 ∈ 𝑉 → 𝑋 ∈ V ) |
9 |
8
|
3ad2ant1 |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝑋 ∈ V ) |
10 |
|
simp3 |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝑍 ⊆ 𝑋 ) |
11 |
9 10
|
ssexd |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝑍 ∈ V ) |
12 |
|
simp2 |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝐹 : 𝑍 –onto→ 𝑌 ) |
13 |
|
fornex |
⊢ ( 𝑍 ∈ V → ( 𝐹 : 𝑍 –onto→ 𝑌 → 𝑌 ∈ V ) ) |
14 |
11 12 13
|
sylc |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → 𝑌 ∈ V ) |
15 |
|
elpw2g |
⊢ ( 𝑌 ∈ V → ( 𝐴 ∈ 𝒫 𝑌 ↔ 𝐴 ⊆ 𝑌 ) ) |
16 |
14 15
|
syl |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐴 ∈ 𝒫 𝑌 ↔ 𝐴 ⊆ 𝑌 ) ) |
17 |
16
|
anbi1d |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( ( 𝐴 ∈ 𝒫 𝑌 ∧ ( ◡ 𝐹 “ 𝐴 ) ∈ 𝐽 ) ↔ ( 𝐴 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝐴 ) ∈ 𝐽 ) ) ) |
18 |
6 17
|
syl5bb |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐴 ∈ { 𝑠 ∈ 𝒫 𝑌 ∣ ( ◡ 𝐹 “ 𝑠 ) ∈ 𝐽 } ↔ ( 𝐴 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝐴 ) ∈ 𝐽 ) ) ) |
19 |
3 18
|
bitrd |
⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐹 : 𝑍 –onto→ 𝑌 ∧ 𝑍 ⊆ 𝑋 ) → ( 𝐴 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝐴 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝐴 ) ∈ 𝐽 ) ) ) |