Theorem coindir

Description: Precomposition with a single-valued class (see cocnv2ssid ) distributes over intersection. (Contributed by BJ, 7-Nov-2026)

	Ref	Expression
Assertion	coindir	$$⊢F\circ F^{-1}\subseteq \mathrm{I}\to \left(A\cap B\right)\circ F=\left(A\circ F\right)\cap \left(B\circ F\right)$$

Proof

Step	Hyp	Ref	Expression
1		coindirss	$$⊢\left(A\cap B\right)\circ F\subseteq \left(A\circ F\right)\cap \left(B\circ F\right)$$
2	1	a1i	$$⊢F\circ F^{-1}\subseteq \mathrm{I}\to \left(A\cap B\right)\circ F\subseteq \left(A\circ F\right)\cap \left(B\circ F\right)$$
3		comodular	$$⊢\left(A\circ F\right)\cap \left(B\circ F\right)\subseteq \left(A\cap \left(\left(B\circ F\right)\circ F^{-1}\right)\right)\circ \left(F\cap \left(A^{-1}\circ \left(B\circ F\right)\right)\right)$$
4		coass	$$⊢\left(B\circ F\right)\circ F^{-1}=B\circ \left(F\circ F^{-1}\right)$$
5		coss2	$$⊢F\circ F^{-1}\subseteq \mathrm{I}\to B\circ \left(F\circ F^{-1}\right)\subseteq B\circ \mathrm{I}$$
6		coi1ss	$$⊢B\circ \mathrm{I}\subseteq B$$
7	5 6	sstrdi	$$⊢F\circ F^{-1}\subseteq \mathrm{I}\to B\circ \left(F\circ F^{-1}\right)\subseteq B$$
8	4 7	eqsstrid	$$⊢F\circ F^{-1}\subseteq \mathrm{I}\to \left(B\circ F\right)\circ F^{-1}\subseteq B$$
9		sslin	$$⊢\left(B\circ F\right)\circ F^{-1}\subseteq B\to A\cap \left(\left(B\circ F\right)\circ F^{-1}\right)\subseteq A\cap B$$
10	8 9	syl	$$⊢F\circ F^{-1}\subseteq \mathrm{I}\to A\cap \left(\left(B\circ F\right)\circ F^{-1}\right)\subseteq A\cap B$$
11		inss1	$$⊢F\cap \left(A^{-1}\circ \left(B\circ F\right)\right)\subseteq F$$
12	11	a1i	$$⊢F\circ F^{-1}\subseteq \mathrm{I}\to F\cap \left(A^{-1}\circ \left(B\circ F\right)\right)\subseteq F$$
13	10 12	coss12d	$$⊢F\circ F^{-1}\subseteq \mathrm{I}\to \left(A\cap \left(\left(B\circ F\right)\circ F^{-1}\right)\right)\circ \left(F\cap \left(A^{-1}\circ \left(B\circ F\right)\right)\right)\subseteq \left(A\cap B\right)\circ F$$
14	3 13	sstrid	$$⊢F\circ F^{-1}\subseteq \mathrm{I}\to \left(A\circ F\right)\cap \left(B\circ F\right)\subseteq \left(A\cap B\right)\circ F$$
15	2 14	eqssd	$$⊢F\circ F^{-1}\subseteq \mathrm{I}\to \left(A\cap B\right)\circ F=\left(A\circ F\right)\cap \left(B\circ F\right)$$