Theorem caofid0r

Description: Transfer a right identity law to the function operation. (Contributed by NM, 21-Oct-2014)

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

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		caofid0r.5	|- ( ( ph /\ x e. S ) -> ( x R B ) = x )
5	2	ffnd	|- ( ph -> F Fn A )
6		fnconstg	|- ( B e. W -> ( A X. { B } ) Fn A )
7	3 6	syl	|- ( ph -> ( A X. { B } ) Fn A )
8		eqidd	|- ( ( ph /\ w e. A ) -> ( F ` w ) = ( F ` w ) )
9		fvconst2g	|- ( ( B e. W /\ w e. A ) -> ( ( A X. { B } ) ` w ) = B )
10	3 9	sylan	|- ( ( ph /\ w e. A ) -> ( ( A X. { B } ) ` w ) = B )
11	4	ralrimiva	|- ( ph -> A. x e. S ( x R B ) = x )
12	2	ffvelcdmda	|- ( ( ph /\ w e. A ) -> ( F ` w ) e. S )
13		oveq1	|- ( x = ( F ` w ) -> ( x R B ) = ( ( F ` w ) R B ) )
14		id	|- ( x = ( F ` w ) -> x = ( F ` w ) )
15	13 14	eqeq12d	|- ( x = ( F ` w ) -> ( ( x R B ) = x <-> ( ( F ` w ) R B ) = ( F ` w ) ) )
16	15	rspccva	|- ( ( A. x e. S ( x R B ) = x /\ ( F ` w ) e. S ) -> ( ( F ` w ) R B ) = ( F ` w ) )
17	11 12 16	syl2an2r	|- ( ( ph /\ w e. A ) -> ( ( F ` w ) R B ) = ( F ` w ) )
18	1 5 7 5 8 10 17	offveq	|- ( ph -> ( F oF R ( A X. { B } ) ) = F )