This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑅 ) )