Theorem relcnvtr

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 𝑅 → ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ↔ ( ◡ 𝑅 ∘ ◡ 𝑅 ) ⊆ ◡ 𝑅 ) )