Theorem cossidres1

Description: If ( B o. A ) is included in the identity relation, then the restriction of B to the range of A is included in the converse of A . (Contributed by BJ, 8-Nov-2026)

	Ref	Expression
Assertion	cossidres1	⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( 𝐵 ↾ ran 𝐴 ) ⊆ ◡ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		coires1	⊢ ( 𝐵 ∘ ( I ↾ ran 𝐴 ) ) = ( 𝐵 ↾ ran 𝐴 )
2		idresrnsscocnv2	⊢ ( I ↾ ran 𝐴 ) ⊆ ( 𝐴 ∘ ◡ 𝐴 )
3		coss2	⊢ ( ( I ↾ ran 𝐴 ) ⊆ ( 𝐴 ∘ ◡ 𝐴 ) → ( 𝐵 ∘ ( I ↾ ran 𝐴 ) ) ⊆ ( 𝐵 ∘ ( 𝐴 ∘ ◡ 𝐴 ) ) )
4	2 3	ax-mp	⊢ ( 𝐵 ∘ ( I ↾ ran 𝐴 ) ) ⊆ ( 𝐵 ∘ ( 𝐴 ∘ ◡ 𝐴 ) )
5		coass	⊢ ( ( 𝐵 ∘ 𝐴 ) ∘ ◡ 𝐴 ) = ( 𝐵 ∘ ( 𝐴 ∘ ◡ 𝐴 ) )
6		coss1	⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( ( 𝐵 ∘ 𝐴 ) ∘ ◡ 𝐴 ) ⊆ ( I ∘ ◡ 𝐴 ) )
7		coi2ss	⊢ ( I ∘ ◡ 𝐴 ) ⊆ ◡ 𝐴
8	6 7	sstrdi	⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( ( 𝐵 ∘ 𝐴 ) ∘ ◡ 𝐴 ) ⊆ ◡ 𝐴 )
9	5 8	eqsstrrid	⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( 𝐵 ∘ ( 𝐴 ∘ ◡ 𝐴 ) ) ⊆ ◡ 𝐴 )
10	4 9	sstrid	⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( 𝐵 ∘ ( I ↾ ran 𝐴 ) ) ⊆ ◡ 𝐴 )
11	1 10	eqsstrrid	⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( 𝐵 ↾ ran 𝐴 ) ⊆ ◡ 𝐴 )