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	$$⊢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 V$$
	qliftval.4	$$⊢x=C\to A=B$$
	qliftval.6	$$⊢\phi \to \mathrm{Fun}F$$
Assertion	qliftval	$$⊢\left(\phi \wedge C\in X\right)\to F\left(\left[C\right]R\right)=B$$

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 V$$
5		qliftval.4	$$⊢x=C\to A=B$$
6		qliftval.6	$$⊢\phi \to \mathrm{Fun}F$$
7	1 2 3 4	qliftlem	$$⊢\left(\phi \wedge x\in X\right)\to \left[x\right]R\in \left(X/R\right)$$
8		eceq1	$$⊢x=C\to \left[x\right]R=\left[C\right]R$$
9	1 7 2 8 5 6	fliftval	$$⊢\left(\phi \wedge C\in X\right)\to F\left(\left[C\right]R\right)=B$$