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 \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)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$class R$
1	0	wtrrel	$wff TrRel R$
2	0	cdm	$class dom R$
3	0	crn	$class ran R$
4	2 3	cxp	$class (dom R \times ran R)$
5	0 4	cin	$class (R \cap (dom R \times ran R))$
6	5 5	ccom	$class ((R \cap (dom R \times ran R)) \circ (R \cap (dom R \times ran R)))$
7	6 5	wss	$wff (R \cap (dom R \times ran R)) \circ (R \cap (dom R \times ran R)) \subseteq R \cap (dom R \times ran R)$
8	0	wrel	$wff Rel R$
9	7 8	wa	$wff ((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)$
10	1 9	wb	$wff (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))$

Metamath Proof Explorer

Definition df-trrel

Detailed syntax breakdown