Theorem fliftval

Description: The value of the function F . (Contributed by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Hypotheses	flift.1	|- F = ran ( x e. X |-> <. A , B >. )
	flift.2	|- ( ( ph /\ x e. X ) -> A e. R )
	flift.3	|- ( ( ph /\ x e. X ) -> B e. S )
	fliftval.4	|- ( x = Y -> A = C )
	fliftval.5	|- ( x = Y -> B = D )
	fliftval.6	|- ( ph -> Fun F )
Assertion	fliftval	|- ( ( ph /\ Y e. X ) -> ( F ` C ) = D )

Proof

Step	Hyp	Ref	Expression
1		flift.1	|- F = ran ( x e. X |-> <. A , B >. )
2		flift.2	|- ( ( ph /\ x e. X ) -> A e. R )
3		flift.3	|- ( ( ph /\ x e. X ) -> B e. S )
4		fliftval.4	|- ( x = Y -> A = C )
5		fliftval.5	|- ( x = Y -> B = D )
6		fliftval.6	|- ( ph -> Fun F )
7	6	adantr	|- ( ( ph /\ Y e. X ) -> Fun F )
8		simpr	|- ( ( ph /\ Y e. X ) -> Y e. X )
9		eqidd	|- ( ph -> D = D )
10		eqidd	|- ( Y e. X -> C = C )
11	9 10	anim12ci	|- ( ( ph /\ Y e. X ) -> ( C = C /\ D = D ) )
12	4	eqeq2d	|- ( x = Y -> ( C = A <-> C = C ) )
13	5	eqeq2d	|- ( x = Y -> ( D = B <-> D = D ) )
14	12 13	anbi12d	|- ( x = Y -> ( ( C = A /\ D = B ) <-> ( C = C /\ D = D ) ) )
15	14	rspcev	|- ( ( Y e. X /\ ( C = C /\ D = D ) ) -> E. x e. X ( C = A /\ D = B ) )
16	8 11 15	syl2anc	|- ( ( ph /\ Y e. X ) -> E. x e. X ( C = A /\ D = B ) )
17	1 2 3	fliftel	|- ( ph -> ( C F D <-> E. x e. X ( C = A /\ D = B ) ) )
18	17	adantr	|- ( ( ph /\ Y e. X ) -> ( C F D <-> E. x e. X ( C = A /\ D = B ) ) )
19	16 18	mpbird	|- ( ( ph /\ Y e. X ) -> C F D )
20		funbrfv	|- ( Fun F -> ( C F D -> ( F ` C ) = D ) )
21	7 19 20	sylc	|- ( ( ph /\ Y e. X ) -> ( F ` C ) = D )