Theorem idresrnsscocnv2

Description: A class precomposed with its converse includes the identity relation restricted to its range. (Contributed by BJ, 25-Oct-2026)

	Ref	Expression
Assertion	idresrnsscocnv2	⊢ ( I ↾ ran 𝐴 ) ⊆ ( 𝐴 ∘ ◡ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		idresdmsscocnv1	⊢ ( I ↾ dom ◡ 𝐴 ) ⊆ ( ◡ ◡ 𝐴 ∘ ◡ 𝐴 )
2		df-rn	⊢ ran 𝐴 = dom ◡ 𝐴
3	2	eqcomi	⊢ dom ◡ 𝐴 = ran 𝐴
4	3	reseq2i	⊢ ( I ↾ dom ◡ 𝐴 ) = ( I ↾ ran 𝐴 )
5		cocnvcnv1	⊢ ( ◡ ◡ 𝐴 ∘ ◡ 𝐴 ) = ( 𝐴 ∘ ◡ 𝐴 )
6	1 4 5	3sstr3i	⊢ ( I ↾ ran 𝐴 ) ⊆ ( 𝐴 ∘ ◡ 𝐴 )