Description: Define the converse reflexive relation predicate (read: R is a converse reflexive relation), see also the comment of dfcnvrefrel3 . Alternate definitions are dfcnvrefrel2 and dfcnvrefrel3 . (Contributed by Peter Mazsa, 16-Jul-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-cnvrefrel | |- ( CnvRefRel R <-> ( ( R i^i ( dom R X. ran R ) ) C_ ( _I i^i ( dom R X. ran R ) ) /\ Rel R ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cR | |- R |
|
| 1 | 0 | wcnvrefrel | |- CnvRefRel R |
| 2 | 0 | cdm | |- dom R |
| 3 | 0 | crn | |- ran R |
| 4 | 2 3 | cxp | |- ( dom R X. ran R ) |
| 5 | 0 4 | cin | |- ( R i^i ( dom R X. ran R ) ) |
| 6 | cid | |- _I |
|
| 7 | 6 4 | cin | |- ( _I i^i ( dom R X. ran R ) ) |
| 8 | 5 7 | wss | |- ( R i^i ( dom R X. ran R ) ) C_ ( _I i^i ( dom R X. ran R ) ) |
| 9 | 0 | wrel | |- Rel R |
| 10 | 8 9 | wa | |- ( ( R i^i ( dom R X. ran R ) ) C_ ( _I i^i ( dom R X. ran R ) ) /\ Rel R ) |
| 11 | 1 10 | wb | |- ( CnvRefRel R <-> ( ( R i^i ( dom R X. ran R ) ) C_ ( _I i^i ( dom R X. ran R ) ) /\ Rel R ) ) |