Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-trrel Structured version   Visualization version   GIF version

Definition df-trrel 35846
Description: Define the transitive relation predicate. (Read: 𝑅 is a transitive relation.) For sets, being an element of the class of transitive relations (df-trrels 35845) is equivalent to satisfying the transitive relation predicate, see eltrrelsrel 35853. Alternate definitions are dftrrel2 35849 and dftrrel3 35850. (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
StepHypRef Expression
1 cR . . 3 class 𝑅
21wtrrel 35504 . 2 wff TrRel 𝑅
31cdm 5531 . . . . . . 7 class dom 𝑅
41crn 5532 . . . . . . 7 class ran 𝑅
53, 4cxp 5529 . . . . . 6 class (dom 𝑅 × ran 𝑅)
61, 5cin 3912 . . . . 5 class (𝑅 ∩ (dom 𝑅 × ran 𝑅))
76, 6ccom 5535 . . . 4 class ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅)))
87, 6wss 3913 . . 3 wff ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅))
91wrel 5536 . . 3 wff Rel 𝑅
108, 9wa 398 . 2 wff (((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)
112, 10wb 208 1 wff ( TrRel 𝑅 ↔ (((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Colors of variables: wff setvar class
This definition is referenced by:  dftrrel2  35849
  Copyright terms: Public domain W3C validator