Theorem rnin

Description: The range of an intersection belongs the intersection of ranges. Theorem 9 of Suppes p. 60. (Contributed by NM, 15-Sep-2004)

	Ref	Expression
Assertion	rnin	$$⊢\mathrm{ran}\left(A\cap B\right)\subseteq \mathrm{ran}A\cap \mathrm{ran}B$$

Proof

Step	Hyp	Ref	Expression
1		cnvin	$$⊢{\left(A\cap B\right)}^{-1}=A^{-1}\cap B^{-1}$$
2	1	dmeqi	$$⊢\mathrm{dom}{\left(A\cap B\right)}^{-1}=\mathrm{dom}\left(A^{-1}\cap B^{-1}\right)$$
3		dmin	$$⊢\mathrm{dom}\left(A^{-1}\cap B^{-1}\right)\subseteq \mathrm{dom}{A}^{-1}\cap \mathrm{dom}{B}^{-1}$$
4	2 3	eqsstri	$$⊢\mathrm{dom}{\left(A\cap B\right)}^{-1}\subseteq \mathrm{dom}{A}^{-1}\cap \mathrm{dom}{B}^{-1}$$
5		df-rn	$$⊢\mathrm{ran}\left(A\cap B\right)=\mathrm{dom}{\left(A\cap B\right)}^{-1}$$
6		df-rn	$$⊢\mathrm{ran}A=\mathrm{dom}{A}^{-1}$$
7		df-rn	$$⊢\mathrm{ran}B=\mathrm{dom}{B}^{-1}$$
8	6 7	ineq12i	$$⊢\mathrm{ran}A\cap \mathrm{ran}B=\mathrm{dom}{A}^{-1}\cap \mathrm{dom}{B}^{-1}$$
9	4 5 8	3sstr4i	$$⊢\mathrm{ran}\left(A\cap B\right)\subseteq \mathrm{ran}A\cap \mathrm{ran}B$$