Theorem cossididresb

Description: When B is single-valued (see cocnv2ssid ) and A is injective (see cocnv1ssid ) , the composition ( B o. A ) is included in the identity relation if and only if ( A o. B ) includes the identity relation restricted to ( dom B i^i ran A ) . (Contributed by BJ, 8-Nov-2026)

	Ref	Expression
Assertion	cossididresb	⊢ ( ( ( 𝐵 ∘ ◡ 𝐵 ) ⊆ I ∧ ( ◡ 𝐴 ∘ 𝐴 ) ⊆ I ) → ( ( 𝐵 ∘ 𝐴 ) ⊆ I ↔ ( I ↾ ( dom 𝐵 ∩ ran 𝐴 ) ) ⊆ ( 𝐴 ∘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cossididres	⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( I ↾ ( dom 𝐵 ∩ ran 𝐴 ) ) ⊆ ( 𝐴 ∘ 𝐵 ) )
2		cnvss	⊢ ( ( I ↾ ( dom 𝐵 ∩ ran 𝐴 ) ) ⊆ ( 𝐴 ∘ 𝐵 ) → ◡ ( I ↾ ( dom 𝐵 ∩ ran 𝐴 ) ) ⊆ ◡ ( 𝐴 ∘ 𝐵 ) )
3		cnvresid	⊢ ◡ ( I ↾ ( dom 𝐵 ∩ ran 𝐴 ) ) = ( I ↾ ( dom 𝐵 ∩ ran 𝐴 ) )
4		cnvco	⊢ ◡ ( 𝐴 ∘ 𝐵 ) = ( ◡ 𝐵 ∘ ◡ 𝐴 )
5	2 3 4	3sstr3g	⊢ ( ( I ↾ ( dom 𝐵 ∩ ran 𝐴 ) ) ⊆ ( 𝐴 ∘ 𝐵 ) → ( I ↾ ( dom 𝐵 ∩ ran 𝐴 ) ) ⊆ ( ◡ 𝐵 ∘ ◡ 𝐴 ) )
6		cossidmid	⊢ ( ( ( 𝐵 ∘ ◡ 𝐵 ) ⊆ I ∧ ( ◡ 𝐴 ∘ 𝐴 ) ⊆ I ) → ( ( I ↾ ( dom 𝐵 ∩ ran 𝐴 ) ) ⊆ ( ◡ 𝐵 ∘ ◡ 𝐴 ) → ( 𝐵 ∘ 𝐴 ) ⊆ I ) )
7	5 6	syl5	⊢ ( ( ( 𝐵 ∘ ◡ 𝐵 ) ⊆ I ∧ ( ◡ 𝐴 ∘ 𝐴 ) ⊆ I ) → ( ( I ↾ ( dom 𝐵 ∩ ran 𝐴 ) ) ⊆ ( 𝐴 ∘ 𝐵 ) → ( 𝐵 ∘ 𝐴 ) ⊆ I ) )
8	1 7	impbid2	⊢ ( ( ( 𝐵 ∘ ◡ 𝐵 ) ⊆ I ∧ ( ◡ 𝐴 ∘ 𝐴 ) ⊆ I ) → ( ( 𝐵 ∘ 𝐴 ) ⊆ I ↔ ( I ↾ ( dom 𝐵 ∩ ran 𝐴 ) ) ⊆ ( 𝐴 ∘ 𝐵 ) ) )