dftrrels2

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 \in Rels \| r \circ r \subseteq r\}$

Proof

Step	Hyp	Ref	Expression
1		df-trrels	$⊢ TrRels = Trs \cap Rels$
2		df-trs	$⊢ Trs = \{r \| ((r \cap (dom r \times ran r)) \circ (r \cap (dom r \times ran r))) S (r \cap (dom r \times ran r))\}$
3		inex1g	$⊢ r \in V \to r \cap (dom r \times ran r) \in V$
4	3	elv	$⊢ r \cap (dom r \times ran r) \in V$
5		brssr	$⊢ r \cap (dom r \times ran r) \in V \to (((r \cap (dom r \times ran r)) \circ (r \cap (dom r \times ran r))) S (r \cap (dom r \times ran r)) \leftrightarrow (r \cap (dom r \times ran r)) \circ (r \cap (dom r \times ran r)) \subseteq r \cap (dom r \times ran r))$
6	4 5	ax-mp	$⊢ ((r \cap (dom r \times ran r)) \circ (r \cap (dom r \times ran r))) S (r \cap (dom r \times ran r)) \leftrightarrow (r \cap (dom r \times ran r)) \circ (r \cap (dom r \times ran r)) \subseteq r \cap (dom r \times ran r)$
7		elrels6	$⊢ r \in V \to (r \in Rels \leftrightarrow r \cap (dom r \times ran r) = r)$
8	7	elv	$⊢ r \in Rels \leftrightarrow r \cap (dom r \times ran r) = r$
9	8	biimpi	$⊢ r \in Rels \to r \cap (dom r \times ran r) = r$
10	9 9	coeq12d	$⊢ r \in Rels \to (r \cap (dom r \times ran r)) \circ (r \cap (dom r \times ran r)) = r \circ r$
11	10 9	sseq12d	$⊢ r \in Rels \to ((r \cap (dom r \times ran r)) \circ (r \cap (dom r \times ran r)) \subseteq r \cap (dom r \times ran r) \leftrightarrow r \circ r \subseteq r)$
12	6 11	syl5bb	$⊢ r \in Rels \to (((r \cap (dom r \times ran r)) \circ (r \cap (dom r \times ran r))) S (r \cap (dom r \times ran r)) \leftrightarrow r \circ r \subseteq r)$
13	1 2 12	abeqinbi	$⊢ TrRels = \{r \in Rels \| r \circ r \subseteq r\}$

Metamath Proof Explorer

Theorem dftrrels2

Proof