Theorem coidmid

Description: A composition that includes the identity relation on the relevant class can be inserted in the middle of a composition. (Contributed by BJ, 8-Nov-2026)

	Ref	Expression
Assertion	coidmid	⊢ ( ( I ↾ ( dom 𝐴 ∩ ran 𝐷 ) ) ⊆ ( 𝐵 ∘ 𝐶 ) → ( 𝐴 ∘ 𝐷 ) ⊆ ( ( 𝐴 ∘ 𝐵 ) ∘ ( 𝐶 ∘ 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		coss2	⊢ ( ( I ↾ ( dom 𝐴 ∩ ran 𝐷 ) ) ⊆ ( 𝐵 ∘ 𝐶 ) → ( 𝐴 ∘ ( I ↾ ( dom 𝐴 ∩ ran 𝐷 ) ) ) ⊆ ( 𝐴 ∘ ( 𝐵 ∘ 𝐶 ) ) )
2		coss1	⊢ ( ( 𝐴 ∘ ( I ↾ ( dom 𝐴 ∩ ran 𝐷 ) ) ) ⊆ ( 𝐴 ∘ ( 𝐵 ∘ 𝐶 ) ) → ( ( 𝐴 ∘ ( I ↾ ( dom 𝐴 ∩ ran 𝐷 ) ) ) ∘ 𝐷 ) ⊆ ( ( 𝐴 ∘ ( 𝐵 ∘ 𝐶 ) ) ∘ 𝐷 ) )
3	1 2	syl	⊢ ( ( I ↾ ( dom 𝐴 ∩ ran 𝐷 ) ) ⊆ ( 𝐵 ∘ 𝐶 ) → ( ( 𝐴 ∘ ( I ↾ ( dom 𝐴 ∩ ran 𝐷 ) ) ) ∘ 𝐷 ) ⊆ ( ( 𝐴 ∘ ( 𝐵 ∘ 𝐶 ) ) ∘ 𝐷 ) )
4		coires1	⊢ ( 𝐴 ∘ ( I ↾ ( dom 𝐴 ∩ ran 𝐷 ) ) ) = ( 𝐴 ↾ ( dom 𝐴 ∩ ran 𝐷 ) )
5		incom	⊢ ( dom 𝐴 ∩ ran 𝐷 ) = ( ran 𝐷 ∩ dom 𝐴 )
6	5	reseq2i	⊢ ( 𝐴 ↾ ( dom 𝐴 ∩ ran 𝐷 ) ) = ( 𝐴 ↾ ( ran 𝐷 ∩ dom 𝐴 ) )
7		resindm	⊢ ( 𝐴 ↾ ( ran 𝐷 ∩ dom 𝐴 ) ) = ( 𝐴 ↾ ran 𝐷 )
8	6 7	eqtri	⊢ ( 𝐴 ↾ ( dom 𝐴 ∩ ran 𝐷 ) ) = ( 𝐴 ↾ ran 𝐷 )
9	4 8	eqtri	⊢ ( 𝐴 ∘ ( I ↾ ( dom 𝐴 ∩ ran 𝐷 ) ) ) = ( 𝐴 ↾ ran 𝐷 )
10	9	coeq1i	⊢ ( ( 𝐴 ∘ ( I ↾ ( dom 𝐴 ∩ ran 𝐷 ) ) ) ∘ 𝐷 ) = ( ( 𝐴 ↾ ran 𝐷 ) ∘ 𝐷 )
11		coresrn	⊢ ( ( 𝐴 ↾ ran 𝐷 ) ∘ 𝐷 ) = ( 𝐴 ∘ 𝐷 )
12	10 11	eqtri	⊢ ( ( 𝐴 ∘ ( I ↾ ( dom 𝐴 ∩ ran 𝐷 ) ) ) ∘ 𝐷 ) = ( 𝐴 ∘ 𝐷 )
13		coass	⊢ ( ( 𝐴 ∘ 𝐵 ) ∘ 𝐶 ) = ( 𝐴 ∘ ( 𝐵 ∘ 𝐶 ) )
14	13	coeq1i	⊢ ( ( ( 𝐴 ∘ 𝐵 ) ∘ 𝐶 ) ∘ 𝐷 ) = ( ( 𝐴 ∘ ( 𝐵 ∘ 𝐶 ) ) ∘ 𝐷 )
15		coass	⊢ ( ( ( 𝐴 ∘ 𝐵 ) ∘ 𝐶 ) ∘ 𝐷 ) = ( ( 𝐴 ∘ 𝐵 ) ∘ ( 𝐶 ∘ 𝐷 ) )
16	14 15	eqtr3i	⊢ ( ( 𝐴 ∘ ( 𝐵 ∘ 𝐶 ) ) ∘ 𝐷 ) = ( ( 𝐴 ∘ 𝐵 ) ∘ ( 𝐶 ∘ 𝐷 ) )
17	3 12 16	3sstr3g	⊢ ( ( I ↾ ( dom 𝐴 ∩ ran 𝐷 ) ) ⊆ ( 𝐵 ∘ 𝐶 ) → ( 𝐴 ∘ 𝐷 ) ⊆ ( ( 𝐴 ∘ 𝐵 ) ∘ ( 𝐶 ∘ 𝐷 ) ) )