Metamath Proof Explorer

Definition df-trrel

Description: Define the transitive relation predicate. (Read: R is a transitive relation.) For sets, being an element of the class of transitive relations ( df-trrels ) is equivalent to satisfying the transitive relation predicate, see eltrrelsrel . Alternate definitions are dftrrel2 and dftrrel3 . (Contributed by Peter Mazsa, 17-Jul-2021)

Ref Expression
Assertion df-trrel 
|- ( TrRel R <-> ( ( ( R i^i ( dom R X. ran R ) ) o. ( R 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 wtrrel 
 |-  TrRel 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 5 5 ccom 
 |-  ( ( R i^i ( dom R X. ran R ) ) o. ( R i^i ( dom R X. ran R ) ) )
7 6 5 wss 
 |-  ( ( R i^i ( dom R X. ran R ) ) o. ( R i^i ( dom R X. ran R ) ) ) C_ ( R i^i ( dom R X. ran R ) )
8 0 wrel 
 |-  Rel R
9 7 8 wa 
 |-  ( ( ( R i^i ( dom R X. ran R ) ) o. ( R i^i ( dom R X. ran R ) ) ) C_ ( R i^i ( dom R X. ran R ) ) /\ Rel R )
10 1 9 wb 
 |-  ( TrRel R <-> ( ( ( R i^i ( dom R X. ran R ) ) o. ( R i^i ( dom R X. ran R ) ) ) C_ ( R i^i ( dom R X. ran R ) ) /\ Rel R ) )