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

Metamath Proof Explorer

Theorem imainrect

Description: Image by a restricted and corestricted binary relation (intersection of a binary relation with a Cartesian product). (Contributed by Stefan O'Rear, 19-Feb-2015)

Ref Expression
Assertion imainrect 
|- ( ( G i^i ( A X. B ) ) " Y ) = ( ( G " ( Y i^i A ) ) i^i B )

Proof

Step Hyp Ref Expression
1 df-res 
 |-  ( ( G i^i ( A X. B ) ) |` Y ) = ( ( G i^i ( A X. B ) ) i^i ( Y X. _V ) )
2 1 rneqi 
 |-  ran ( ( G i^i ( A X. B ) ) |` Y ) = ran ( ( G i^i ( A X. B ) ) i^i ( Y X. _V ) )
3 df-ima 
 |-  ( ( G i^i ( A X. B ) ) " Y ) = ran ( ( G i^i ( A X. B ) ) |` Y )
4 df-ima 
 |-  ( G " ( Y i^i A ) ) = ran ( G |` ( Y i^i A ) )
5 df-res 
 |-  ( G |` ( Y i^i A ) ) = ( G i^i ( ( Y i^i A ) X. _V ) )
6 5 rneqi 
 |-  ran ( G |` ( Y i^i A ) ) = ran ( G i^i ( ( Y i^i A ) X. _V ) )
7 4 6 eqtri 
 |-  ( G " ( Y i^i A ) ) = ran ( G i^i ( ( Y i^i A ) X. _V ) )
8 7 ineq1i 
 |-  ( ( G " ( Y i^i A ) ) i^i B ) = ( ran ( G i^i ( ( Y i^i A ) X. _V ) ) i^i B )
9 cnvin 
 |-  `' ( ( G i^i ( ( Y i^i A ) X. _V ) ) i^i ( _V X. B ) ) = ( `' ( G i^i ( ( Y i^i A ) X. _V ) ) i^i `' ( _V X. B ) )
10 inxp 
 |-  ( ( A X. _V ) i^i ( _V X. B ) ) = ( ( A i^i _V ) X. ( _V i^i B ) )
11 inv1 
 |-  ( A i^i _V ) = A
12 incom 
 |-  ( _V i^i B ) = ( B i^i _V )
13 inv1 
 |-  ( B i^i _V ) = B
14 12 13 eqtri 
 |-  ( _V i^i B ) = B
15 11 14 xpeq12i 
 |-  ( ( A i^i _V ) X. ( _V i^i B ) ) = ( A X. B )
16 10 15 eqtr2i 
 |-  ( A X. B ) = ( ( A X. _V ) i^i ( _V X. B ) )
17 16 ineq2i 
 |-  ( ( G i^i ( Y X. _V ) ) i^i ( A X. B ) ) = ( ( G i^i ( Y X. _V ) ) i^i ( ( A X. _V ) i^i ( _V X. B ) ) )
18 in32 
 |-  ( ( G i^i ( A X. B ) ) i^i ( Y X. _V ) ) = ( ( G i^i ( Y X. _V ) ) i^i ( A X. B ) )
19 xpindir 
 |-  ( ( Y i^i A ) X. _V ) = ( ( Y X. _V ) i^i ( A X. _V ) )
20 19 ineq2i 
 |-  ( G i^i ( ( Y i^i A ) X. _V ) ) = ( G i^i ( ( Y X. _V ) i^i ( A X. _V ) ) )
21 inass 
 |-  ( ( G i^i ( Y X. _V ) ) i^i ( A X. _V ) ) = ( G i^i ( ( Y X. _V ) i^i ( A X. _V ) ) )
22 20 21 eqtr4i 
 |-  ( G i^i ( ( Y i^i A ) X. _V ) ) = ( ( G i^i ( Y X. _V ) ) i^i ( A X. _V ) )
23 22 ineq1i 
 |-  ( ( G i^i ( ( Y i^i A ) X. _V ) ) i^i ( _V X. B ) ) = ( ( ( G i^i ( Y X. _V ) ) i^i ( A X. _V ) ) i^i ( _V X. B ) )
24 inass 
 |-  ( ( ( G i^i ( Y X. _V ) ) i^i ( A X. _V ) ) i^i ( _V X. B ) ) = ( ( G i^i ( Y X. _V ) ) i^i ( ( A X. _V ) i^i ( _V X. B ) ) )
25 23 24 eqtri 
 |-  ( ( G i^i ( ( Y i^i A ) X. _V ) ) i^i ( _V X. B ) ) = ( ( G i^i ( Y X. _V ) ) i^i ( ( A X. _V ) i^i ( _V X. B ) ) )
26 17 18 25 3eqtr4i 
 |-  ( ( G i^i ( A X. B ) ) i^i ( Y X. _V ) ) = ( ( G i^i ( ( Y i^i A ) X. _V ) ) i^i ( _V X. B ) )
27 26 cnveqi 
 |-  `' ( ( G i^i ( A X. B ) ) i^i ( Y X. _V ) ) = `' ( ( G i^i ( ( Y i^i A ) X. _V ) ) i^i ( _V X. B ) )
28 df-res 
 |-  ( `' ( G i^i ( ( Y i^i A ) X. _V ) ) |` B ) = ( `' ( G i^i ( ( Y i^i A ) X. _V ) ) i^i ( B X. _V ) )
29 cnvxp 
 |-  `' ( _V X. B ) = ( B X. _V )
30 29 ineq2i 
 |-  ( `' ( G i^i ( ( Y i^i A ) X. _V ) ) i^i `' ( _V X. B ) ) = ( `' ( G i^i ( ( Y i^i A ) X. _V ) ) i^i ( B X. _V ) )
31 28 30 eqtr4i 
 |-  ( `' ( G i^i ( ( Y i^i A ) X. _V ) ) |` B ) = ( `' ( G i^i ( ( Y i^i A ) X. _V ) ) i^i `' ( _V X. B ) )
32 9 27 31 3eqtr4ri 
 |-  ( `' ( G i^i ( ( Y i^i A ) X. _V ) ) |` B ) = `' ( ( G i^i ( A X. B ) ) i^i ( Y X. _V ) )
33 32 dmeqi 
 |-  dom ( `' ( G i^i ( ( Y i^i A ) X. _V ) ) |` B ) = dom `' ( ( G i^i ( A X. B ) ) i^i ( Y X. _V ) )
34 incom 
 |-  ( B i^i dom `' ( G i^i ( ( Y i^i A ) X. _V ) ) ) = ( dom `' ( G i^i ( ( Y i^i A ) X. _V ) ) i^i B )
35 dmres 
 |-  dom ( `' ( G i^i ( ( Y i^i A ) X. _V ) ) |` B ) = ( B i^i dom `' ( G i^i ( ( Y i^i A ) X. _V ) ) )
36 df-rn 
 |-  ran ( G i^i ( ( Y i^i A ) X. _V ) ) = dom `' ( G i^i ( ( Y i^i A ) X. _V ) )
37 36 ineq1i 
 |-  ( ran ( G i^i ( ( Y i^i A ) X. _V ) ) i^i B ) = ( dom `' ( G i^i ( ( Y i^i A ) X. _V ) ) i^i B )
38 34 35 37 3eqtr4ri 
 |-  ( ran ( G i^i ( ( Y i^i A ) X. _V ) ) i^i B ) = dom ( `' ( G i^i ( ( Y i^i A ) X. _V ) ) |` B )
39 df-rn 
 |-  ran ( ( G i^i ( A X. B ) ) i^i ( Y X. _V ) ) = dom `' ( ( G i^i ( A X. B ) ) i^i ( Y X. _V ) )
40 33 38 39 3eqtr4ri 
 |-  ran ( ( G i^i ( A X. B ) ) i^i ( Y X. _V ) ) = ( ran ( G i^i ( ( Y i^i A ) X. _V ) ) i^i B )
41 8 40 eqtr4i 
 |-  ( ( G " ( Y i^i A ) ) i^i B ) = ran ( ( G i^i ( A X. B ) ) i^i ( Y X. _V ) )
42 2 3 41 3eqtr4i 
 |-  ( ( G i^i ( A X. B ) ) " Y ) = ( ( G " ( Y i^i A ) ) i^i B )