Metamath Proof Explorer


Theorem qliftlem

Description: Lemma for theorems about a function lift. (Contributed by Mario Carneiro, 23-Dec-2016) (Revised by AV, 3-Aug-2024)

Ref Expression
Hypotheses qlift.1 F = ran x X x R A
qlift.2 φ x X A Y
qlift.3 φ R Er X
qlift.4 φ X V
Assertion qliftlem φ x X x R X / R

Proof

Step Hyp Ref Expression
1 qlift.1 F = ran x X x R A
2 qlift.2 φ x X A Y
3 qlift.3 φ R Er X
4 qlift.4 φ X V
5 erex R Er X X V R V
6 3 4 5 sylc φ R V
7 ecelqsg R V x X x R X / R
8 6 7 sylan φ x X x R X / R