Metamath Proof Explorer


Theorem qliftval

Description: The value 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 ( 𝜑𝑋𝑉 )
qliftval.4 ( 𝑥 = 𝐶𝐴 = 𝐵 )
qliftval.6 ( 𝜑 → Fun 𝐹 )
Assertion qliftval ( ( 𝜑𝐶𝑋 ) → ( 𝐹 ‘ [ 𝐶 ] 𝑅 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 qlift.1 𝐹 = ran ( 𝑥𝑋 ↦ ⟨ [ 𝑥 ] 𝑅 , 𝐴 ⟩ )
2 qlift.2 ( ( 𝜑𝑥𝑋 ) → 𝐴𝑌 )
3 qlift.3 ( 𝜑𝑅 Er 𝑋 )
4 qlift.4 ( 𝜑𝑋𝑉 )
5 qliftval.4 ( 𝑥 = 𝐶𝐴 = 𝐵 )
6 qliftval.6 ( 𝜑 → Fun 𝐹 )
7 1 2 3 4 qliftlem ( ( 𝜑𝑥𝑋 ) → [ 𝑥 ] 𝑅 ∈ ( 𝑋 / 𝑅 ) )
8 eceq1 ( 𝑥 = 𝐶 → [ 𝑥 ] 𝑅 = [ 𝐶 ] 𝑅 )
9 1 7 2 8 5 6 fliftval ( ( 𝜑𝐶𝑋 ) → ( 𝐹 ‘ [ 𝐶 ] 𝑅 ) = 𝐵 )