Metamath Proof Explorer


Definition df-refrel

Description: Define the reflexive relation predicate. (Read: R is a reflexive relation.) This is a surprising definition, see the comment of dfrefrel3 . Alternate definitions are dfrefrel2 and dfrefrel3 . For sets, being an element of the class of reflexive relations ( df-refrels ) is equivalent to satisfying the reflexive relation predicate, that is ( R e. RefRels <-> RefRel R ) when R is a set, see elrefrelsrel . (Contributed by Peter Mazsa, 16-Jul-2021)

Ref Expression
Assertion df-refrel
|- ( RefRel R <-> ( ( _I i^i ( dom R X. ran R ) ) C_ ( R i^i ( dom R X. ran R ) ) /\ Rel R ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR
 |-  R
1 0 wrefrel
 |-  RefRel R
2 cid
 |-  _I
3 0 cdm
 |-  dom R
4 0 crn
 |-  ran R
5 3 4 cxp
 |-  ( dom R X. ran R )
6 2 5 cin
 |-  ( _I i^i ( dom R X. ran R ) )
7 0 5 cin
 |-  ( R i^i ( dom R X. ran R ) )
8 6 7 wss
 |-  ( _I i^i ( dom R X. ran R ) ) C_ ( R i^i ( dom R X. ran R ) )
9 0 wrel
 |-  Rel R
10 8 9 wa
 |-  ( ( _I i^i ( dom R X. ran R ) ) C_ ( R i^i ( dom R X. ran R ) ) /\ Rel R )
11 1 10 wb
 |-  ( RefRel R <-> ( ( _I i^i ( dom R X. ran R ) ) C_ ( R i^i ( dom R X. ran R ) ) /\ Rel R ) )