Theorem caofid0r

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

	Ref	Expression
Hypotheses	caofref.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	caofref.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
	caofid0.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	caofid0r.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 𝑅 𝐵 ) = 𝑥 )
Assertion	caofid0r	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 ( 𝐴 × { 𝐵 } ) ) = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		caofref.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		caofref.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
3		caofid0.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
4		caofid0r.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 𝑅 𝐵 ) = 𝑥 )
5	2	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
6		fnconstg	⊢ ( 𝐵 ∈ 𝑊 → ( 𝐴 × { 𝐵 } ) Fn 𝐴 )
7	3 6	syl	⊢ ( 𝜑 → ( 𝐴 × { 𝐵 } ) Fn 𝐴 )
8		eqidd	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
9		fvconst2g	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑤 ) = 𝐵 )
10	3 9	sylan	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑤 ) = 𝐵 )
11	4	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ( 𝑥 𝑅 𝐵 ) = 𝑥 )
12	2	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 )
13		oveq1	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( 𝑥 𝑅 𝐵 ) = ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝐵 ) )
14		id	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → 𝑥 = ( 𝐹 ‘ 𝑤 ) )
15	13 14	eqeq12d	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( ( 𝑥 𝑅 𝐵 ) = 𝑥 ↔ ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝐵 ) = ( 𝐹 ‘ 𝑤 ) ) )
16	15	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝑆 ( 𝑥 𝑅 𝐵 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝐵 ) = ( 𝐹 ‘ 𝑤 ) )
17	11 12 16	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝐵 ) = ( 𝐹 ‘ 𝑤 ) )
18	1 5 7 5 8 10 17	offveq	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 ( 𝐴 × { 𝐵 } ) ) = 𝐹 )