Metamath Proof Explorer


Theorem fvrcllb0d

Description: A restriction of the identity relation is a subset of the reflexive closure of a set. (Contributed by RP, 22-Jul-2020)

Ref Expression
Hypothesis fvrcllb0d.r
|- ( ph -> R e. _V )
Assertion fvrcllb0d
|- ( ph -> ( _I |` ( dom R u. ran R ) ) C_ ( r* ` R ) )

Proof

Step Hyp Ref Expression
1 fvrcllb0d.r
 |-  ( ph -> R e. _V )
2 dfrcl4
 |-  r* = ( r e. _V |-> U_ n e. { 0 , 1 } ( r ^r n ) )
3 prex
 |-  { 0 , 1 } e. _V
4 3 a1i
 |-  ( ph -> { 0 , 1 } e. _V )
5 c0ex
 |-  0 e. _V
6 5 prid1
 |-  0 e. { 0 , 1 }
7 6 a1i
 |-  ( ph -> 0 e. { 0 , 1 } )
8 2 1 4 7 fvmptiunrelexplb0d
 |-  ( ph -> ( _I |` ( dom R u. ran R ) ) C_ ( r* ` R ) )