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 ( ( 𝐺 ∩ ( 𝐴 × 𝐵 ) ) “ 𝑌 ) = ( ( 𝐺 “ ( 𝑌 ∩ 𝐴 ) ) ∩ 𝐵 )

Proof

Step Hyp Ref Expression
1 df-res ⊢ ( ( 𝐺 ∩ ( 𝐴 × 𝐵 ) ) ↾ 𝑌 ) = ( ( 𝐺 ∩ ( 𝐴 × 𝐵 ) ) ∩ ( 𝑌 × V ) )
2 1 rneqi ⊢ ran ( ( 𝐺 ∩ ( 𝐴 × 𝐵 ) ) ↾ 𝑌 ) = ran ( ( 𝐺 ∩ ( 𝐴 × 𝐵 ) ) ∩ ( 𝑌 × V ) )
3 df-ima ⊢ ( ( 𝐺 ∩ ( 𝐴 × 𝐵 ) ) “ 𝑌 ) = ran ( ( 𝐺 ∩ ( 𝐴 × 𝐵 ) ) ↾ 𝑌 )
4 df-ima ⊢ ( 𝐺 “ ( 𝑌 ∩ 𝐴 ) ) = ran ( 𝐺 ↾ ( 𝑌 ∩ 𝐴 ) )
5 df-res ⊢ ( 𝐺 ↾ ( 𝑌 ∩ 𝐴 ) ) = ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) )
6 5 rneqi ⊢ ran ( 𝐺 ↾ ( 𝑌 ∩ 𝐴 ) ) = ran ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) )
7 4 6 eqtri ⊢ ( 𝐺 “ ( 𝑌 ∩ 𝐴 ) ) = ran ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) )
8 7 ineq1i ⊢ ( ( 𝐺 “ ( 𝑌 ∩ 𝐴 ) ) ∩ 𝐵 ) = ( ran ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) ∩ 𝐵 )
9 cnvin ⊢ ◡ ( ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) ∩ ( V × 𝐵 ) ) = ( ◡ ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) ∩ ◡ ( V × 𝐵 ) )
10 inxp ⊢ ( ( 𝐴 × V ) ∩ ( V × 𝐵 ) ) = ( ( 𝐴 ∩ V ) × ( V ∩ 𝐵 ) )
11 inv1 ⊢ ( 𝐴 ∩ V ) = 𝐴
12 incom ⊢ ( V ∩ 𝐵 ) = ( 𝐵 ∩ V )
13 inv1 ⊢ ( 𝐵 ∩ V ) = 𝐵
14 12 13 eqtri ⊢ ( V ∩ 𝐵 ) = 𝐵
15 11 14 xpeq12i ⊢ ( ( 𝐴 ∩ V ) × ( V ∩ 𝐵 ) ) = ( 𝐴 × 𝐵 )
16 10 15 eqtr2i ⊢ ( 𝐴 × 𝐵 ) = ( ( 𝐴 × V ) ∩ ( V × 𝐵 ) )
17 16 ineq2i ⊢ ( ( 𝐺 ∩ ( 𝑌 × V ) ) ∩ ( 𝐴 × 𝐵 ) ) = ( ( 𝐺 ∩ ( 𝑌 × V ) ) ∩ ( ( 𝐴 × V ) ∩ ( V × 𝐵 ) ) )
18 in32 ⊢ ( ( 𝐺 ∩ ( 𝐴 × 𝐵 ) ) ∩ ( 𝑌 × V ) ) = ( ( 𝐺 ∩ ( 𝑌 × V ) ) ∩ ( 𝐴 × 𝐵 ) )
19 xpindir ⊢ ( ( 𝑌 ∩ 𝐴 ) × V ) = ( ( 𝑌 × V ) ∩ ( 𝐴 × V ) )
20 19 ineq2i ⊢ ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) = ( 𝐺 ∩ ( ( 𝑌 × V ) ∩ ( 𝐴 × V ) ) )
21 inass ⊢ ( ( 𝐺 ∩ ( 𝑌 × V ) ) ∩ ( 𝐴 × V ) ) = ( 𝐺 ∩ ( ( 𝑌 × V ) ∩ ( 𝐴 × V ) ) )
22 20 21 eqtr4i ⊢ ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) = ( ( 𝐺 ∩ ( 𝑌 × V ) ) ∩ ( 𝐴 × V ) )
23 22 ineq1i ⊢ ( ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) ∩ ( V × 𝐵 ) ) = ( ( ( 𝐺 ∩ ( 𝑌 × V ) ) ∩ ( 𝐴 × V ) ) ∩ ( V × 𝐵 ) )
24 inass ⊢ ( ( ( 𝐺 ∩ ( 𝑌 × V ) ) ∩ ( 𝐴 × V ) ) ∩ ( V × 𝐵 ) ) = ( ( 𝐺 ∩ ( 𝑌 × V ) ) ∩ ( ( 𝐴 × V ) ∩ ( V × 𝐵 ) ) )
25 23 24 eqtri ⊢ ( ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) ∩ ( V × 𝐵 ) ) = ( ( 𝐺 ∩ ( 𝑌 × V ) ) ∩ ( ( 𝐴 × V ) ∩ ( V × 𝐵 ) ) )
26 17 18 25 3eqtr4i ⊢ ( ( 𝐺 ∩ ( 𝐴 × 𝐵 ) ) ∩ ( 𝑌 × V ) ) = ( ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) ∩ ( V × 𝐵 ) )
27 26 cnveqi ⊢ ◡ ( ( 𝐺 ∩ ( 𝐴 × 𝐵 ) ) ∩ ( 𝑌 × V ) ) = ◡ ( ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) ∩ ( V × 𝐵 ) )
28 df-res ⊢ ( ◡ ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) ↾ 𝐵 ) = ( ◡ ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) ∩ ( 𝐵 × V ) )
29 cnvxp ⊢ ◡ ( V × 𝐵 ) = ( 𝐵 × V )
30 29 ineq2i ⊢ ( ◡ ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) ∩ ◡ ( V × 𝐵 ) ) = ( ◡ ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) ∩ ( 𝐵 × V ) )
31 28 30 eqtr4i ⊢ ( ◡ ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) ↾ 𝐵 ) = ( ◡ ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) ∩ ◡ ( V × 𝐵 ) )
32 9 27 31 3eqtr4ri ⊢ ( ◡ ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) ↾ 𝐵 ) = ◡ ( ( 𝐺 ∩ ( 𝐴 × 𝐵 ) ) ∩ ( 𝑌 × V ) )
33 32 dmeqi ⊢ dom ( ◡ ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) ↾ 𝐵 ) = dom ◡ ( ( 𝐺 ∩ ( 𝐴 × 𝐵 ) ) ∩ ( 𝑌 × V ) )
34 incom ⊢ ( 𝐵 ∩ dom ◡ ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) ) = ( dom ◡ ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) ∩ 𝐵 )
35 dmres ⊢ dom ( ◡ ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) ↾ 𝐵 ) = ( 𝐵 ∩ dom ◡ ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) )
36 df-rn ⊢ ran ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) = dom ◡ ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) )
37 36 ineq1i ⊢ ( ran ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) ∩ 𝐵 ) = ( dom ◡ ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) ∩ 𝐵 )
38 34 35 37 3eqtr4ri ⊢ ( ran ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) ∩ 𝐵 ) = dom ( ◡ ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) ↾ 𝐵 )
39 df-rn ⊢ ran ( ( 𝐺 ∩ ( 𝐴 × 𝐵 ) ) ∩ ( 𝑌 × V ) ) = dom ◡ ( ( 𝐺 ∩ ( 𝐴 × 𝐵 ) ) ∩ ( 𝑌 × V ) )
40 33 38 39 3eqtr4ri ⊢ ran ( ( 𝐺 ∩ ( 𝐴 × 𝐵 ) ) ∩ ( 𝑌 × V ) ) = ( ran ( 𝐺 ∩ ( ( 𝑌 ∩ 𝐴 ) × V ) ) ∩ 𝐵 )
41 8 40 eqtr4i ⊢ ( ( 𝐺 “ ( 𝑌 ∩ 𝐴 ) ) ∩ 𝐵 ) = ran ( ( 𝐺 ∩ ( 𝐴 × 𝐵 ) ) ∩ ( 𝑌 × V ) )
42 2 3 41 3eqtr4i ⊢ ( ( 𝐺 ∩ ( 𝐴 × 𝐵 ) ) “ 𝑌 ) = ( ( 𝐺 “ ( 𝑌 ∩ 𝐴 ) ) ∩ 𝐵 )