Metamath Proof Explorer

Theorem dftrrel3

Description: Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021)

Ref Expression
Assertion dftrrel3 ⊢ TrRel R ↔ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z ∧ Rel ⁡ R

Proof

Step Hyp Ref Expression
1 dftrrel2 ⊢ TrRel R ↔ R ∘ R ⊆ R ∧ Rel ⁡ R
2 cotr ⊢ R ∘ R ⊆ R ↔ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z
3 2 anbi1i ⊢ R ∘ R ⊆ R ∧ Rel ⁡ R ↔ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z ∧ Rel ⁡ R
4 1 3 bitri ⊢ TrRel R ↔ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z ∧ Rel ⁡ R