Metamath Proof Explorer


Theorem qliftf

Description: The domain and range of the function F . (Contributed by Mario Carneiro, 23-Dec-2016) (Revised by AV, 3-Aug-2024)

Ref Expression
Hypotheses qlift.1 𝐹 = ran ( 𝑥𝑋 ↦ ⟨ [ 𝑥 ] 𝑅 , 𝐴 ⟩ )
qlift.2 ( ( 𝜑𝑥𝑋 ) → 𝐴𝑌 )
qlift.3 ( 𝜑𝑅 Er 𝑋 )
qlift.4 ( 𝜑𝑋𝑉 )
Assertion qliftf ( 𝜑 → ( Fun 𝐹𝐹 : ( 𝑋 / 𝑅 ) ⟶ 𝑌 ) )

Proof

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 𝐹𝐹 : ( 𝑋 / 𝑅 ) ⟶ 𝑌 ) )