Definition df-trrel 38575

Description: Define the transitive relation predicate. (Read: 𝑅 is a transitive relation.) For sets, being an element of the class of transitive relations (df-trrels 38574) is equivalent to satisfying the transitive relation predicate, see eltrrelsrel 38582. Alternate definitions are dftrrel2 38578 and dftrrel3 38579. (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 38197	. 2 wff TrRel 𝑅
3	1	cdm 5685	. . . . . . 7 class dom 𝑅
4	1	crn 5686	. . . . . . 7 class ran 𝑅
5	3, 4	cxp 5683	. . . . . 6 class (dom 𝑅 × ran 𝑅)
6	1, 5	cin 3950	. . . . 5 class (𝑅 ∩ (dom 𝑅 × ran 𝑅))
7	6, 6	ccom 5689	. . . 4 class ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅)))
8	7, 6	wss 3951	. . 3 wff ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅))
9	1	wrel 5690	. . 3 wff Rel 𝑅
10	8, 9	wa 395	. 2 wff (((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)
11	2, 10	wb 206	1 wff ( TrRel 𝑅 ↔ (((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))

This definition is referenced by:  dftrrel2  38578