Metamath Proof Explorer


Theorem dftrrels2

Description: Alternate definition of the class of transitive relations.

I'd prefer to define the class of transitive relations by using the definition of composition by Suppes p. 63. df-coSUP ( A o. B ) = { <. x , y >. | E. u ( x A u /\ u B y ) } as opposed to the present definition of composition df-co ( A o. B ) = { <. x , y >. | E. u ( x B u /\ u A y ) } because the Suppes definition keeps the order of A , B , C , R , S , T by default in trsinxpSUP ( ( ( R i^i ( A X. B ) ) o. ( S i^i ( B X. C ) ) ) C_ ( T i^i ( A X. C ) ) <-> A. x e. A A. y e. B A. z e. C ( ( x R y /\ y S z ) -> x T z ) ) while the present definition of composition disarranges them: trsinxp ( ( ( S i^i ( B X. C ) ) o. ( R i^i ( A X. B ) ) ) C_ ( T i^i ( A X. C ) ) <-> A. x e. A A. y e. B A. z e. C ( ( x R y /\ y S z ) -> x T z ) ) . This is not mission critical to me, the implication of the Suppes definition is just more aesthetic, at least in the above case.

If we swap to the Suppes definition of class composition, I would define the present class of all transitive sets as df-trsSUP and I would consider to switch the definition of the class of cosets by R from the present df-coss to a df-cossSUP. But perhaps there is a mathematical reason to keep the present definition of composition. (Contributed by Peter Mazsa, 21-Jul-2021)

Ref Expression
Assertion dftrrels2 TrRels = r Rels | r r r

Proof

Step Hyp Ref Expression
1 df-trrels TrRels = Trs Rels
2 df-trs Trs = r | r dom r × ran r r dom r × ran r S r dom r × ran r
3 inex1g r V r dom r × ran r V
4 3 elv r dom r × ran r V
5 brssr r dom r × ran r V r dom r × ran r r dom r × ran r S r dom r × ran r r dom r × ran r r dom r × ran r r dom r × ran r
6 4 5 ax-mp r dom r × ran r r dom r × ran r S r dom r × ran r r dom r × ran r r dom r × ran r r dom r × ran r
7 elrels6 r V r Rels r dom r × ran r = r
8 7 elv r Rels r dom r × ran r = r
9 8 biimpi r Rels r dom r × ran r = r
10 9 9 coeq12d r Rels r dom r × ran r r dom r × ran r = r r
11 10 9 sseq12d r Rels r dom r × ran r r dom r × ran r r dom r × ran r r r r
12 6 11 syl5bb r Rels r dom r × ran r r dom r × ran r S r dom r × ran r r r r
13 1 2 12 abeqinbi TrRels = r Rels | r r r