Metamath Proof Explorer

Theorem eltrrels3

Description: Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021)

Ref Expression
Assertion eltrrels3 ⊢ R ∈ TrRels ↔ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z ∧ R ∈ Rels

Proof

Step Hyp Ref Expression
1 dftrrels3 ⊢ TrRels = r ∈ Rels | ∀ x ∀ y ∀ z x r y ∧ y r z → x r z
2 breq ⊢ r = R → x r y ↔ x R y
3 breq ⊢ r = R → y r z ↔ y R z
4 2 3 anbi12d ⊢ r = R → x r y ∧ y r z ↔ x R y ∧ y R z
5 breq ⊢ r = R → x r z ↔ x R z
6 4 5 imbi12d ⊢ r = R → x r y ∧ y r z → x r z ↔ x R y ∧ y R z → x R z
7 6 2albidv ⊢ r = R → ∀ y ∀ z x r y ∧ y r z → x r z ↔ ∀ y ∀ z x R y ∧ y R z → x R z
8 7 albidv ⊢ r = R → ∀ x ∀ y ∀ z x r y ∧ y r z → x r z ↔ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z
9 1 8 rabeqel ⊢ R ∈ TrRels ↔ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z ∧ R ∈ Rels