Theorem inimass

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

	Ref	Expression
Assertion	inimass	|- ( ( A i^i B ) " C ) C_ ( ( A " C ) i^i ( B " C ) )

Proof

Step	Hyp	Ref	Expression
1		rnin	|- ran ( ( A |` C ) i^i ( B |` C ) ) C_ ( ran ( A |` C ) i^i ran ( B |` C ) )
2		df-ima	|- ( ( A i^i B ) " C ) = ran ( ( A i^i B ) |` C )
3		resindir	|- ( ( A i^i B ) |` C ) = ( ( A |` C ) i^i ( B |` C ) )
4	3	rneqi	|- ran ( ( A i^i B ) |` C ) = ran ( ( A |` C ) i^i ( B |` C ) )
5	2 4	eqtri	|- ( ( A i^i B ) " C ) = ran ( ( A |` C ) i^i ( B |` C ) )
6		df-ima	|- ( A " C ) = ran ( A |` C )
7		df-ima	|- ( B " C ) = ran ( B |` C )
8	6 7	ineq12i	|- ( ( A " C ) i^i ( B " C ) ) = ( ran ( A |` C ) i^i ran ( B |` C ) )
9	1 5 8	3sstr4i	|- ( ( A i^i B ) " C ) C_ ( ( A " C ) i^i ( B " C ) )