Theorem coindirss

Description: Precomposition is subdistributive over intersection. Compare with coundir . See coindir for equality when precomposing with a single-valued class. (Contributed by BJ, 8-Nov-2026)

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

Proof

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