Definition df-trrel

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1	0	wtrrel	⊢ TrRel 𝑅
2	0	cdm	⊢ dom 𝑅
3	0	crn	⊢ ran 𝑅
4	2 3	cxp	⊢ ( dom 𝑅 × ran 𝑅 )
5	0 4	cin	⊢ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) )
6	5 5	ccom	⊢ ( ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) )
7	6 5	wss	⊢ ( ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ) ⊆ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) )
8	0	wrel	⊢ Rel 𝑅
9	7 8	wa	⊢ ( ( ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ) ⊆ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ∧ Rel 𝑅 )
10	1 9	wb	⊢ ( TrRel 𝑅 ↔ ( ( ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ) ⊆ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ∧ Rel 𝑅 ) )