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