Metamath Proof Explorer


Theorem qliftel1

Description: Elementhood in the relation 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 qliftel1 ( ( 𝜑𝑥𝑋 ) → [ 𝑥 ] 𝑅 𝐹 𝐴 )

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 fliftel1 ( ( 𝜑𝑥𝑋 ) → [ 𝑥 ] 𝑅 𝐹 𝐴 )