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