Definition df-trrel 37439

Description: Define the transitive relation predicate. (Read: 𝑅 is a transitive relation.) For sets, being an element of the class of transitive relations (df-trrels 37438) is equivalent to satisfying the transitive relation predicate, see eltrrelsrel 37446. Alternate definitions are dftrrel2 37442 and dftrrel3 37443. (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 37053	. 2 wff TrRel 𝑅
3	1	cdm 5676	. . . . . . 7 class dom 𝑅
4	1	crn 5677	. . . . . . 7 class ran 𝑅
5	3, 4	cxp 5674	. . . . . 6 class (dom 𝑅 × ran 𝑅)
6	1, 5	cin 3947	. . . . 5 class (𝑅 ∩ (dom 𝑅 × ran 𝑅))
7	6, 6	ccom 5680	. . . 4 class ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅)))
8	7, 6	wss 3948	. . 3 wff ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅))
9	1	wrel 5681	. . 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  37442