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 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 𝑅 𝐹 )