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 )