dftrrel2

Description: Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021)

		Ref	Expression
	Assertion	dftrrel2	$⊢ TrRel R \leftrightarrow (R \circ R \subseteq R \land Rel R)$

Step	Hyp	Ref	Expression
1		df-trrel	$⊢ TrRel 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) \land Rel R)$
2		dfrel6	$⊢ Rel R \leftrightarrow R \cap (dom R \times ran R) = R$
3	2	biimpi	$⊢ Rel R \to R \cap (dom R \times ran R) = R$
4	3 3	coeq12d	$⊢ Rel R \to (R \cap (dom R \times ran R)) \circ (R \cap (dom R \times ran R)) = R \circ R$
5	4 3	sseq12d	$⊢ Rel R \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)$
6	5	pm5.32ri	$⊢ ((R \cap (dom R \times ran R)) \circ (R \cap (dom R \times ran R)) \subseteq R \cap (dom R \times ran R) \land Rel R) \leftrightarrow (R \circ R \subseteq R \land Rel R)$
7	1 6	bitri	$⊢ TrRel R \leftrightarrow (R \circ R \subseteq R \land Rel R)$

Metamath Proof Explorer