Theorem coindiss

Description: Postcomposition is subdistributive over intersection. Compare with coundi . See coindi for equality when postcomposing with an injective class. (Contributed by BJ, 8-Nov-2026)

	Ref	Expression
Assertion	coindiss	$$⊢A\circ \left(B\cap C\right)\subseteq \left(A\circ B\right)\cap \left(A\circ C\right)$$

Proof

Step	Hyp	Ref	Expression
1		inss1	$$⊢B\cap C\subseteq B$$
2		coss2	$$⊢B\cap C\subseteq B\to A\circ \left(B\cap C\right)\subseteq A\circ B$$
3	1 2	ax-mp	$$⊢A\circ \left(B\cap C\right)\subseteq A\circ B$$
4		inss2	$$⊢B\cap C\subseteq C$$
5		coss2	$$⊢B\cap C\subseteq C\to A\circ \left(B\cap C\right)\subseteq A\circ C$$
6	4 5	ax-mp	$$⊢A\circ \left(B\cap C\right)\subseteq A\circ C$$
7	3 6	ssini	$$⊢A\circ \left(B\cap C\right)\subseteq \left(A\circ B\right)\cap \left(A\circ C\right)$$