Theorem cotr

Description: Two ways of saying a relation is transitive. Definition of transitivity in Schechter p. 51. Special instance of cotrg . (Contributed by NM, 27-Dec-1996)

	Ref	Expression
Assertion	cotr	⊢ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		cotrg	⊢ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )