Description: Alternate definition of the class of reflexive relations. This is a 0-ary class constant, which is recommended for definitions (see the 1. Guideline at https://us.metamath.org/ileuni/mathbox.html ). Proper classes (like _I , see iprc ) are not elements of this (or any) class: if a class is an element of another class, it is not a proper class but a set, see elex . So if we use 0-ary constant classes as our main definitions, they are valid only for sets, not for proper classes. For proper classes we use predicate-type definitions like df-refrel . See also the comment of df-rels .
Note that while elementhood in the class of relations cancels restriction of r in dfrefrels2 , it keeps restriction of _I : this is why the very similar definitions df-refs , df-syms and df-trs diverge when we switch from (general) sets to relations in dfrefrels2 , dfsymrels2 and dftrrels2 . (Contributed by Peter Mazsa, 20-Jul-2019)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dfrefrels2 | |- RefRels = { r e. Rels | ( _I i^i ( dom r X. ran r ) ) C_ r } |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-refrels | |- RefRels = ( Refs i^i Rels ) |
|
| 2 | df-refs | |- Refs = { r | ( _I i^i ( dom r X. ran r ) ) _S ( r i^i ( dom r X. ran r ) ) } |
|
| 3 | inex1g | |- ( r e. _V -> ( r i^i ( dom r X. ran r ) ) e. _V ) |
|
| 4 | 3 | elv | |- ( r i^i ( dom r X. ran r ) ) e. _V |
| 5 | brssr | |- ( ( r i^i ( dom r X. ran r ) ) e. _V -> ( ( _I i^i ( dom r X. ran r ) ) _S ( r i^i ( dom r X. ran r ) ) <-> ( _I i^i ( dom r X. ran r ) ) C_ ( r i^i ( dom r X. ran r ) ) ) ) |
|
| 6 | 4 5 | ax-mp | |- ( ( _I i^i ( dom r X. ran r ) ) _S ( r i^i ( dom r X. ran r ) ) <-> ( _I i^i ( dom r X. ran r ) ) C_ ( r i^i ( dom r X. ran r ) ) ) |
| 7 | elrels6 | |- ( r e. _V -> ( r e. Rels <-> ( r i^i ( dom r X. ran r ) ) = r ) ) |
|
| 8 | 7 | elv | |- ( r e. Rels <-> ( r i^i ( dom r X. ran r ) ) = r ) |
| 9 | 8 | biimpi | |- ( r e. Rels -> ( r i^i ( dom r X. ran r ) ) = r ) |
| 10 | 9 | sseq2d | |- ( r e. Rels -> ( ( _I i^i ( dom r X. ran r ) ) C_ ( r i^i ( dom r X. ran r ) ) <-> ( _I i^i ( dom r X. ran r ) ) C_ r ) ) |
| 11 | 6 10 | syl5bb | |- ( r e. Rels -> ( ( _I i^i ( dom r X. ran r ) ) _S ( r i^i ( dom r X. ran r ) ) <-> ( _I i^i ( dom r X. ran r ) ) C_ r ) ) |
| 12 | 1 2 11 | abeqinbi | |- RefRels = { r e. Rels | ( _I i^i ( dom r X. ran r ) ) C_ r } |