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