Step |
Hyp |
Ref |
Expression |
1 |
|
qlift.1 |
⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ 〈 [ 𝑥 ] 𝑅 , 𝐴 〉 ) |
2 |
|
qlift.2 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑌 ) |
3 |
|
qlift.3 |
⊢ ( 𝜑 → 𝑅 Er 𝑋 ) |
4 |
|
qlift.4 |
⊢ ( 𝜑 → 𝑋 ∈ 𝑉 ) |
5 |
1 2 3 4
|
qliftlem |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → [ 𝑥 ] 𝑅 ∈ ( 𝑋 / 𝑅 ) ) |
6 |
1 5 2
|
fliftf |
⊢ ( 𝜑 → ( Fun 𝐹 ↔ 𝐹 : ran ( 𝑥 ∈ 𝑋 ↦ [ 𝑥 ] 𝑅 ) ⟶ 𝑌 ) ) |
7 |
|
df-qs |
⊢ ( 𝑋 / 𝑅 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 𝑦 = [ 𝑥 ] 𝑅 } |
8 |
|
eqid |
⊢ ( 𝑥 ∈ 𝑋 ↦ [ 𝑥 ] 𝑅 ) = ( 𝑥 ∈ 𝑋 ↦ [ 𝑥 ] 𝑅 ) |
9 |
8
|
rnmpt |
⊢ ran ( 𝑥 ∈ 𝑋 ↦ [ 𝑥 ] 𝑅 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 𝑦 = [ 𝑥 ] 𝑅 } |
10 |
7 9
|
eqtr4i |
⊢ ( 𝑋 / 𝑅 ) = ran ( 𝑥 ∈ 𝑋 ↦ [ 𝑥 ] 𝑅 ) |
11 |
10
|
a1i |
⊢ ( 𝜑 → ( 𝑋 / 𝑅 ) = ran ( 𝑥 ∈ 𝑋 ↦ [ 𝑥 ] 𝑅 ) ) |
12 |
11
|
feq2d |
⊢ ( 𝜑 → ( 𝐹 : ( 𝑋 / 𝑅 ) ⟶ 𝑌 ↔ 𝐹 : ran ( 𝑥 ∈ 𝑋 ↦ [ 𝑥 ] 𝑅 ) ⟶ 𝑌 ) ) |
13 |
6 12
|
bitr4d |
⊢ ( 𝜑 → ( Fun 𝐹 ↔ 𝐹 : ( 𝑋 / 𝑅 ) ⟶ 𝑌 ) ) |