This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 )
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 𝑅 𝐹 )