Definition df-trrel 35970

Description: Define the transitive relation predicate. (Read: 𝑅 is a transitive relation.) For sets, being an element of the class of transitive relations (df-trrels 35969) is equivalent to satisfying the transitive relation predicate, see eltrrelsrel 35977. Alternate definitions are dftrrel2 35973 and dftrrel3 35974. (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 35628	. 2 wff TrRel 𝑅
3	1	cdm 5519	. . . . . . 7 class dom 𝑅
4	1	crn 5520	. . . . . . 7 class ran 𝑅
5	3, 4	cxp 5517	. . . . . 6 class (dom 𝑅 × ran 𝑅)
6	1, 5	cin 3880	. . . . 5 class (𝑅 ∩ (dom 𝑅 × ran 𝑅))
7	6, 6	ccom 5523	. . . 4 class ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅)))
8	7, 6	wss 3881	. . 3 wff ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅))
9	1	wrel 5524	. . 3 wff Rel 𝑅
10	8, 9	wa 399	. 2 wff (((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)
11	2, 10	wb 209	1 wff ( TrRel 𝑅 ↔ (((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))

This definition is referenced by:  dftrrel2  35973