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	$⊢ ran (A \cap B) \subseteq ran A \cap ran B$

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

Metamath Proof Explorer