Definition df-trrel 35842

Description: Define the transitive relation predicate. (Read: 𝑅 is a transitive relation.) For sets, being an element of the class of transitive relations (df-trrels 35841) is equivalent to satisfying the transitive relation predicate, see eltrrelsrel 35849. Alternate definitions are dftrrel2 35845 and dftrrel3 35846. (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 35500	. 2 wff TrRel 𝑅
3	1	cdm 5541	. . . . . . 7 class dom 𝑅
4	1	crn 5542	. . . . . . 7 class ran 𝑅
5	3, 4	cxp 5539	. . . . . 6 class (dom 𝑅 × ran 𝑅)
6	1, 5	cin 3923	. . . . 5 class (𝑅 ∩ (dom 𝑅 × ran 𝑅))
7	6, 6	ccom 5545	. . . 4 class ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅)))
8	7, 6	wss 3924	. . 3 wff ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅))
9	1	wrel 5546	. . 3 wff Rel 𝑅
10	8, 9	wa 398	. 2 wff (((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)
11	2, 10	wb 208	1 wff ( TrRel 𝑅 ↔ (((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))

This definition is referenced by:  dftrrel2  35845