Theorem dftrrels3

Description: Alternate definition of the class of transitive relations. (Contributed by Peter Mazsa, 22-Jul-2021)

	Ref	Expression
Assertion	dftrrels3	⊢ TrRels = { 𝑟 ∈ Rels ∣ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) }

Proof

Step	Hyp	Ref	Expression
1		dftrrels2	⊢ TrRels = { 𝑟 ∈ Rels ∣ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 }
2		cotr	⊢ ( ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) )
3	1 2	rabbieq	⊢ TrRels = { 𝑟 ∈ Rels ∣ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) }