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 = 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 )
	qliftval.4	|- ( x = C -> A = B )
	qliftval.6	|- ( ph -> Fun F )
Assertion	qliftval	|- ( ( ph /\ C e. X ) -> ( F ` [ C ] R ) = B )

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		qliftval.4	|- ( x = C -> A = B )
6		qliftval.6	|- ( ph -> Fun F )
7	1 2 3 4	qliftlem	|- ( ( ph /\ x e. X ) -> [ x ] R e. ( X /. R ) )
8		eceq1	|- ( x = C -> [ x ] R = [ C ] R )
9	1 7 2 8 5 6	fliftval	|- ( ( ph /\ C e. X ) -> ( F ` [ C ] R ) = B )