Theorem relcnvtrOLD

Description: Obsolete form of relcnvtrg as of 8-Aug-2026. (Contributed by FL, 19-Sep-2011) (Proof shortened by Peter Mazsa, 17-Oct-2023) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	relcnvtrOLD	⊢ ( Rel 𝑅 → ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ↔ ( ◡ 𝑅 ∘ ◡ 𝑅 ) ⊆ ◡ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		3anidm	⊢ ( ( Rel 𝑅 ∧ Rel 𝑅 ∧ Rel 𝑅 ) ↔ Rel 𝑅 )
2		relcnvtrgOLD	⊢ ( ( Rel 𝑅 ∧ Rel 𝑅 ∧ Rel 𝑅 ) → ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ↔ ( ◡ 𝑅 ∘ ◡ 𝑅 ) ⊆ ◡ 𝑅 ) )
3	1 2	sylbir	⊢ ( Rel 𝑅 → ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ↔ ( ◡ 𝑅 ∘ ◡ 𝑅 ) ⊆ ◡ 𝑅 ) )