Description: A restriction of the identity relation is a subset of the reflexive closure of a relation. (Contributed by RP, 22-Jul-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fvrcllb0da.rel | |- ( ph -> Rel R ) |
|
fvrcllb0da.r | |- ( ph -> R e. _V ) |
||
Assertion | fvrcllb0da | |- ( ph -> ( _I |` U. U. R ) C_ ( r* ` R ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvrcllb0da.rel | |- ( ph -> Rel R ) |
|
2 | fvrcllb0da.r | |- ( ph -> R e. _V ) |
|
3 | dfrcl4 | |- r* = ( r e. _V |-> U_ n e. { 0 , 1 } ( r ^r n ) ) |
|
4 | prex | |- { 0 , 1 } e. _V |
|
5 | 4 | a1i | |- ( ph -> { 0 , 1 } e. _V ) |
6 | c0ex | |- 0 e. _V |
|
7 | 6 | prid1 | |- 0 e. { 0 , 1 } |
8 | 7 | a1i | |- ( ph -> 0 e. { 0 , 1 } ) |
9 | 3 2 5 1 8 | fvmptiunrelexplb0da | |- ( ph -> ( _I |` U. U. R ) C_ ( r* ` R ) ) |