Definition df-trrel 36688

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

Assertion

Ref	Expression
df-trrel	⊢ ( TrRel 𝑅 ↔ (((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))

Detailed syntax breakdown of Definition df-trrel

Step	Hyp	Ref	Expression
1		cR	. . 3 class 𝑅
2	1	wtrrel 36348	. 2 wff TrRel 𝑅
3	1	cdm 5589	. . . . . . 7 class dom 𝑅
4	1	crn 5590	. . . . . . 7 class ran 𝑅
5	3, 4	cxp 5587	. . . . . 6 class (dom 𝑅 × ran 𝑅)
6	1, 5	cin 3886	. . . . 5 class (𝑅 ∩ (dom 𝑅 × ran 𝑅))
7	6, 6	ccom 5593	. . . 4 class ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅)))
8	7, 6	wss 3887	. . 3 wff ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅))
9	1	wrel 5594	. . 3 wff Rel 𝑅
10	8, 9	wa 396	. 2 wff (((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)
11	2, 10	wb 205	1 wff ( TrRel 𝑅 ↔ (((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))

This definition is referenced by:  dftrrel2  36691