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 
|- ( ph -> A e. V )
caofref.2 
|- ( ph -> F : A --> S )
caofref.3 
|- ( ( ph /\ x e. S ) -> x R x )
Assertion caofref 
|- ( ph -> F oR R F )

Proof

Step Hyp Ref Expression
1 caofref.1 
 |-  ( ph -> A e. V )
2 caofref.2 
 |-  ( ph -> F : A --> S )
3 caofref.3 
 |-  ( ( ph /\ x e. S ) -> x R x )
4 id 
 |-  ( x = ( F ` w ) -> x = ( F ` w ) )
5 4 4 breq12d 
 |-  ( x = ( F ` w ) -> ( x R x <-> ( F ` w ) R ( F ` w ) ) )
6 3 ralrimiva 
 |-  ( ph -> A. x e. S x R x )
7 6 adantr 
 |-  ( ( ph /\ w e. A ) -> A. x e. S x R x )
8 2 ffvelcdmda 
 |-  ( ( ph /\ w e. A ) -> ( F ` w ) e. S )
9 5 7 8 rspcdva 
 |-  ( ( ph /\ w e. A ) -> ( F ` w ) R ( F ` w ) )
10 9 ralrimiva 
 |-  ( ph -> A. w e. A ( F ` w ) R ( F ` w ) )
11 2 ffnd 
 |-  ( ph -> F Fn A )
12 inidm 
 |-  ( A i^i A ) = A
13 eqidd 
 |-  ( ( ph /\ w e. A ) -> ( F ` w ) = ( F ` w ) )
14 11 11 1 1 12 13 13 ofrfval 
 |-  ( ph -> ( F oR R F <-> A. w e. A ( F ` w ) R ( F ` w ) ) )
15 10 14 mpbird 
 |-  ( ph -> F oR R F )