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 e. X |-> <. [ x ] R , A >. )
	qlift.2	|- ( ( ph /\ x e. X ) -> A e. Y )
	qlift.3	|- ( ph -> R Er X )
	qlift.4	|- ( ph -> X e. V )
Assertion	qliftlem	|- ( ( ph /\ x e. X ) -> [ x ] R e. ( X /. R ) )

Proof

Step	Hyp	Ref	Expression
1		qlift.1	|- F = ran ( x e. X |-> <. [ x ] R , A >. )
2		qlift.2	|- ( ( ph /\ x e. X ) -> A e. Y )
3		qlift.3	|- ( ph -> R Er X )
4		qlift.4	|- ( ph -> X e. V )
5		erex	|- ( R Er X -> ( X e. V -> R e. _V ) )
6	3 4 5	sylc	|- ( ph -> R e. _V )
7		ecelqsg	|- ( ( R e. _V /\ x e. X ) -> [ x ] R e. ( X /. R ) )
8	6 7	sylan	|- ( ( ph /\ x e. X ) -> [ x ] R e. ( X /. R ) )