Theorem caofid2

Description: Transfer a right absorption law to the function operation. (Contributed by Mario Carneiro, 28-Jul-2014)

	Ref	Expression
Hypotheses	caofref.1	|- ( ph -> A e. V )
	caofref.2	|- ( ph -> F : A --> S )
	caofid0.3	|- ( ph -> B e. W )
	caofid1.4	|- ( ph -> C e. X )
	caofid2.5	|- ( ( ph /\ x e. S ) -> ( B R x ) = C )
Assertion	caofid2	|- ( ph -> ( ( A X. { B } ) oF R F ) = ( A X. { C } ) )

Proof

Step	Hyp	Ref	Expression
1		caofref.1	|- ( ph -> A e. V )
2		caofref.2	|- ( ph -> F : A --> S )
3		caofid0.3	|- ( ph -> B e. W )
4		caofid1.4	|- ( ph -> C e. X )
5		caofid2.5	|- ( ( ph /\ x e. S ) -> ( B R x ) = C )
6		fnconstg	|- ( B e. W -> ( A X. { B } ) Fn A )
7	3 6	syl	|- ( ph -> ( A X. { B } ) Fn A )
8	2	ffnd	|- ( ph -> F Fn A )
9		fnconstg	|- ( C e. X -> ( A X. { C } ) Fn A )
10	4 9	syl	|- ( ph -> ( A X. { C } ) Fn A )
11		fvconst2g	|- ( ( B e. W /\ w e. A ) -> ( ( A X. { B } ) ` w ) = B )
12	3 11	sylan	|- ( ( ph /\ w e. A ) -> ( ( A X. { B } ) ` w ) = B )
13		eqidd	|- ( ( ph /\ w e. A ) -> ( F ` w ) = ( F ` w ) )
14	5	ralrimiva	|- ( ph -> A. x e. S ( B R x ) = C )
15	2	ffvelcdmda	|- ( ( ph /\ w e. A ) -> ( F ` w ) e. S )
16		oveq2	|- ( x = ( F ` w ) -> ( B R x ) = ( B R ( F ` w ) ) )
17	16	eqeq1d	|- ( x = ( F ` w ) -> ( ( B R x ) = C <-> ( B R ( F ` w ) ) = C ) )
18	17	rspccva	|- ( ( A. x e. S ( B R x ) = C /\ ( F ` w ) e. S ) -> ( B R ( F ` w ) ) = C )
19	14 15 18	syl2an2r	|- ( ( ph /\ w e. A ) -> ( B R ( F ` w ) ) = C )
20		fvconst2g	|- ( ( C e. X /\ w e. A ) -> ( ( A X. { C } ) ` w ) = C )
21	4 20	sylan	|- ( ( ph /\ w e. A ) -> ( ( A X. { C } ) ` w ) = C )
22	19 21	eqtr4d	|- ( ( ph /\ w e. A ) -> ( B R ( F ` w ) ) = ( ( A X. { C } ) ` w ) )
23	1 7 8 10 12 13 22	offveq	|- ( ph -> ( ( A X. { B } ) oF R F ) = ( A X. { C } ) )