Theorem cossidmid

Description: If ( A o. B ) and ( C o. D ) are included in the identity relation and ( B o. C ) includes it on ( dom A i^i ran D ) , then ( A o. D ) is included in the identity relation. (Contributed by BJ, 8-Nov-2026)

	Ref	Expression
Assertion	cossidmid	$$⊢\left(A\circ B\subseteq \mathrm{I}\wedge C\circ D\subseteq \mathrm{I}\right)\to \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cap \mathrm{ran}D\right)}\subseteq B\circ C\to A\circ D\subseteq \mathrm{I}\right)$$

Proof

Step	Hyp	Ref	Expression
1		coidmid	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cap \mathrm{ran}D\right)}\subseteq B\circ C\to A\circ D\subseteq \left(A\circ B\right)\circ \left(C\circ D\right)$$
2		simpl	$$⊢\left(A\circ B\subseteq \mathrm{I}\wedge C\circ D\subseteq \mathrm{I}\right)\to A\circ B\subseteq \mathrm{I}$$
3		simpr	$$⊢\left(A\circ B\subseteq \mathrm{I}\wedge C\circ D\subseteq \mathrm{I}\right)\to C\circ D\subseteq \mathrm{I}$$
4	2 3	coss12d	$$⊢\left(A\circ B\subseteq \mathrm{I}\wedge C\circ D\subseteq \mathrm{I}\right)\to \left(A\circ B\right)\circ \left(C\circ D\right)\subseteq \mathrm{I}\circ \mathrm{I}$$
5		reli	$$⊢\mathrm{Rel}\mathrm{I}$$
6		coi1	$$⊢\mathrm{Rel}\mathrm{I}\to \mathrm{I}\circ \mathrm{I}=\mathrm{I}$$
7	5 6	ax-mp	$$⊢\mathrm{I}\circ \mathrm{I}=\mathrm{I}$$
8	4 7	sseqtrdi	$$⊢\left(A\circ B\subseteq \mathrm{I}\wedge C\circ D\subseteq \mathrm{I}\right)\to \left(A\circ B\right)\circ \left(C\circ D\right)\subseteq \mathrm{I}$$
9	1 8	sylan9ssr	$$⊢\left(\left(A\circ B\subseteq \mathrm{I}\wedge C\circ D\subseteq \mathrm{I}\right)\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cap \mathrm{ran}D\right)}\subseteq B\circ C\right)\to A\circ D\subseteq \mathrm{I}$$
10	9	ex	$$⊢\left(A\circ B\subseteq \mathrm{I}\wedge C\circ D\subseteq \mathrm{I}\right)\to \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cap \mathrm{ran}D\right)}\subseteq B\circ C\to A\circ D\subseteq \mathrm{I}\right)$$