Theorem cotr2

Description: Two ways of saying a relation is transitive. Special instance of cotr2g . (Contributed by RP, 22-Mar-2020)

	Ref	Expression
Hypotheses	cotr2.a	⊢ dom 𝑅 ⊆ 𝐴
	cotr2.b	⊢ ( dom 𝑅 ∩ ran 𝑅 ) ⊆ 𝐵
	cotr2.c	⊢ ran 𝑅 ⊆ 𝐶
Assertion	cotr2	⊢ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		cotr2.a	⊢ dom 𝑅 ⊆ 𝐴
2		cotr2.b	⊢ ( dom 𝑅 ∩ ran 𝑅 ) ⊆ 𝐵
3		cotr2.c	⊢ ran 𝑅 ⊆ 𝐶
4		incom	⊢ ( dom 𝑅 ∩ ran 𝑅 ) = ( ran 𝑅 ∩ dom 𝑅 )
5	4 2	eqsstrri	⊢ ( ran 𝑅 ∩ dom 𝑅 ) ⊆ 𝐵
6	1 5 3	cotr2g	⊢ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )