This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )