This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: A relation is transitive iff its converse is transitive. (Contributed by FL, 19-Sep-2011) (Proof shortened by Peter Mazsa, 17-Oct-2023)
|
|
Ref |
Expression |
|
Assertion |
relcnvtr |
⊢ ( Rel 𝑅 → ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ↔ ( ◡ 𝑅 ∘ ◡ 𝑅 ) ⊆ ◡ 𝑅 ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
3anidm |
⊢ ( ( Rel 𝑅 ∧ Rel 𝑅 ∧ Rel 𝑅 ) ↔ Rel 𝑅 ) |
| 2 |
|
relcnvtrg |
⊢ ( ( Rel 𝑅 ∧ Rel 𝑅 ∧ Rel 𝑅 ) → ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ↔ ( ◡ 𝑅 ∘ ◡ 𝑅 ) ⊆ ◡ 𝑅 ) ) |
| 3 |
1 2
|
sylbir |
⊢ ( Rel 𝑅 → ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ↔ ( ◡ 𝑅 ∘ ◡ 𝑅 ) ⊆ ◡ 𝑅 ) ) |