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

Metamath Proof Explorer

Theorem idref

Description: Two ways to state that a relation is reflexive on a class. (Contributed by FL, 15-Jan-2012) (Proof shortened by Mario Carneiro, 3-Nov-2015) (Revised by NM, 30-Mar-2016)

Ref Expression
Assertion idref 
|- ( ( _I |` A ) C_ R <-> A. x e. A x R x )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( x e. A |-> <. x , x >. ) = ( x e. A |-> <. x , x >. )
2 1 fmpt 
 |-  ( A. x e. A <. x , x >. e. R <-> ( x e. A |-> <. x , x >. ) : A --> R )
3 opex 
 |-  <. x , x >. e. _V
4 3 1 fnmpti 
 |-  ( x e. A |-> <. x , x >. ) Fn A
5 df-f 
 |-  ( ( x e. A |-> <. x , x >. ) : A --> R <-> ( ( x e. A |-> <. x , x >. ) Fn A /\ ran ( x e. A |-> <. x , x >. ) C_ R ) )
6 4 5 mpbiran 
 |-  ( ( x e. A |-> <. x , x >. ) : A --> R <-> ran ( x e. A |-> <. x , x >. ) C_ R )
7 2 6 bitri 
 |-  ( A. x e. A <. x , x >. e. R <-> ran ( x e. A |-> <. x , x >. ) C_ R )
8 df-br 
 |-  ( x R x <-> <. x , x >. e. R )
9 8 ralbii 
 |-  ( A. x e. A x R x <-> A. x e. A <. x , x >. e. R )
10 mptresid 
 |-  ( _I |` A ) = ( x e. A |-> x )
11 vex 
 |-  x e. _V
12 11 fnasrn 
 |-  ( x e. A |-> x ) = ran ( x e. A |-> <. x , x >. )
13 10 12 eqtri 
 |-  ( _I |` A ) = ran ( x e. A |-> <. x , x >. )
14 13 sseq1i 
 |-  ( ( _I |` A ) C_ R <-> ran ( x e. A |-> <. x , x >. ) C_ R )
15 7 9 14 3bitr4ri 
 |-  ( ( _I |` A ) C_ R <-> A. x e. A x R x )