inimass

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

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

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

Metamath Proof Explorer