This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )