Theorem qliftlem

Description: F , a function lift, is a subset of R X. S . (Contributed by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Hypotheses	qlift.1	$$⊢F=\mathrm{ran}\left(x\in X⟼⟨\left[x\right]R,A⟩\right)$$
	qlift.2	$$⊢\left(\phi \wedge x\in X\right)\to A\in Y$$
	qlift.3	$$⊢\phi \to R\mathrm{Er}X$$
	qlift.4	$$⊢\phi \to X\in \mathrm{V}$$
Assertion	qliftlem	$$⊢\left(\phi \wedge x\in X\right)\to \left[x\right]R\in \left(X/R\right)$$

Proof

Step	Hyp	Ref	Expression
1		qlift.1	$$⊢F=\mathrm{ran}\left(x\in X⟼⟨\left[x\right]R,A⟩\right)$$
2		qlift.2	$$⊢\left(\phi \wedge x\in X\right)\to A\in Y$$
3		qlift.3	$$⊢\phi \to R\mathrm{Er}X$$
4		qlift.4	$$⊢\phi \to X\in \mathrm{V}$$
5		erex	$$⊢R\mathrm{Er}X\to \left(X\in \mathrm{V}\to R\in \mathrm{V}\right)$$
6	3 4 5	sylc	$$⊢\phi \to R\in \mathrm{V}$$
7		ecelqsg	$$⊢\left(R\in \mathrm{V}\wedge x\in X\right)\to \left[x\right]R\in \left(X/R\right)$$
8	6 7	sylan	$$⊢\left(\phi \wedge x\in X\right)\to \left[x\right]R\in \left(X/R\right)$$