Theorem inimass

Description: The image of an intersection. (Contributed by Thierry Arnoux, 16-Dec-2017)

	Ref	Expression
Assertion	inimass	$$⊢\left(A\cap B\right)\left[C\right]\subseteq A\left[C\right]\cap B\left[C\right]$$

Proof

Step	Hyp	Ref	Expression
1		rnin	$$⊢\mathrm{ran}\left(\left({A\upharpoonright }_C\right)\cap \left({B\upharpoonright }_C\right)\right)\subseteq \mathrm{ran}\left({A\upharpoonright }_C\right)\cap \mathrm{ran}\left({B\upharpoonright }_C\right)$$
2		df-ima	$$⊢\left(A\cap B\right)\left[C\right]=\mathrm{ran}\left({\left(A\cap B\right)\upharpoonright }_C\right)$$
3		resindir	$$⊢{\left(A\cap B\right)\upharpoonright }_C=\left({A\upharpoonright }_C\right)\cap \left({B\upharpoonright }_C\right)$$
4	3	rneqi	$$⊢\mathrm{ran}\left({\left(A\cap B\right)\upharpoonright }_C\right)=\mathrm{ran}\left(\left({A\upharpoonright }_C\right)\cap \left({B\upharpoonright }_C\right)\right)$$
5	2 4	eqtri	$$⊢\left(A\cap B\right)\left[C\right]=\mathrm{ran}\left(\left({A\upharpoonright }_C\right)\cap \left({B\upharpoonright }_C\right)\right)$$
6		df-ima	$$⊢A\left[C\right]=\mathrm{ran}\left({A\upharpoonright }_C\right)$$
7		df-ima	$$⊢B\left[C\right]=\mathrm{ran}\left({B\upharpoonright }_C\right)$$
8	6 7	ineq12i	$$⊢A\left[C\right]\cap B\left[C\right]=\mathrm{ran}\left({A\upharpoonright }_C\right)\cap \mathrm{ran}\left({B\upharpoonright }_C\right)$$
9	1 5 8	3sstr4i	$$⊢\left(A\cap B\right)\left[C\right]\subseteq A\left[C\right]\cap B\left[C\right]$$