Theorem caofref

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

	Ref	Expression
Hypotheses	caofref.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	caofref.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
	caofref.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 𝑅 𝑥 )
Assertion	caofref	⊢ ( 𝜑 → 𝐹 ∘r 𝑅 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		caofref.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		caofref.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
3		caofref.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 𝑅 𝑥 )
4		id	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → 𝑥 = ( 𝐹 ‘ 𝑤 ) )
5	4 4	breq12d	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( 𝑥 𝑅 𝑥 ↔ ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑤 ) ) )
6	3	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 𝑥 𝑅 𝑥 )
7	6	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝑆 𝑥 𝑅 𝑥 )
8	2	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 )
9	5 7 8	rspcdva	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑤 ) )
10	9	ralrimiva	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐴 ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑤 ) )
11	2	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
12		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
13		eqidd	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
14	11 11 1 1 12 13 13	ofrfval	⊢ ( 𝜑 → ( 𝐹 ∘r 𝑅 𝐹 ↔ ∀ 𝑤 ∈ 𝐴 ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑤 ) ) )
15	10 14	mpbird	⊢ ( 𝜑 → 𝐹 ∘r 𝑅 𝐹 )