Metamath Proof Explorer

Theorem fimaproj

Description: Image of a cartesian product for a function on ordered pairs with values expressed as ordered pairs. Note that F and G are the projections of H to the first and second coordinate respectively. (Contributed by Thierry Arnoux, 30-Dec-2019)

Ref Expression
Hypotheses fvproj.h 
|- H = ( x e. A , y e. B |-> <. ( F ` x ) , ( G ` y ) >. )
fimaproj.f 
|- ( ph -> F Fn A )
fimaproj.g 
|- ( ph -> G Fn B )
fimaproj.x 
|- ( ph -> X C_ A )
fimaproj.y 
|- ( ph -> Y C_ B )
Assertion fimaproj 
|- ( ph -> ( H " ( X X. Y ) ) = ( ( F " X ) X. ( G " Y ) ) )

Proof

Step Hyp Ref Expression
1 fvproj.h 
 |-  H = ( x e. A , y e. B |-> <. ( F ` x ) , ( G ` y ) >. )
2 fimaproj.f 
 |-  ( ph -> F Fn A )
3 fimaproj.g 
 |-  ( ph -> G Fn B )
4 fimaproj.x 
 |-  ( ph -> X C_ A )
5 fimaproj.y 
 |-  ( ph -> Y C_ B )
6 opex 
 |-  <. ( F ` ( 1st ` z ) ) , ( G ` ( 2nd ` z ) ) >. e. _V
7 vex 
 |-  x e. _V
8 vex 
 |-  y e. _V
9 7 8 op1std 
 |-  ( z = <. x , y >. -> ( 1st ` z ) = x )
10 9 fveq2d 
 |-  ( z = <. x , y >. -> ( F ` ( 1st ` z ) ) = ( F ` x ) )
11 7 8 op2ndd 
 |-  ( z = <. x , y >. -> ( 2nd ` z ) = y )
12 11 fveq2d 
 |-  ( z = <. x , y >. -> ( G ` ( 2nd ` z ) ) = ( G ` y ) )
13 10 12 opeq12d 
 |-  ( z = <. x , y >. -> <. ( F ` ( 1st ` z ) ) , ( G ` ( 2nd ` z ) ) >. = <. ( F ` x ) , ( G ` y ) >. )
14 13 mpompt 
 |-  ( z e. ( A X. B ) |-> <. ( F ` ( 1st ` z ) ) , ( G ` ( 2nd ` z ) ) >. ) = ( x e. A , y e. B |-> <. ( F ` x ) , ( G ` y ) >. )
15 1 14 eqtr4i 
 |-  H = ( z e. ( A X. B ) |-> <. ( F ` ( 1st ` z ) ) , ( G ` ( 2nd ` z ) ) >. )
16 6 15 fnmpti 
 |-  H Fn ( A X. B )
17 xpss12 
 |-  ( ( X C_ A /\ Y C_ B ) -> ( X X. Y ) C_ ( A X. B ) )
18 4 5 17 syl2anc 
 |-  ( ph -> ( X X. Y ) C_ ( A X. B ) )
19 fvelimab 
 |-  ( ( H Fn ( A X. B ) /\ ( X X. Y ) C_ ( A X. B ) ) -> ( c e. ( H " ( X X. Y ) ) <-> E. z e. ( X X. Y ) ( H ` z ) = c ) )
20 16 18 19 sylancr 
 |-  ( ph -> ( c e. ( H " ( X X. Y ) ) <-> E. z e. ( X X. Y ) ( H ` z ) = c ) )
21 simp-4r 
 |-  ( ( ( ( ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) /\ a e. X ) /\ ( F ` a ) = ( 1st ` c ) ) /\ b e. Y ) /\ ( G ` b ) = ( 2nd ` c ) ) -> a e. X )
22 simplr 
 |-  ( ( ( ( ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) /\ a e. X ) /\ ( F ` a ) = ( 1st ` c ) ) /\ b e. Y ) /\ ( G ` b ) = ( 2nd ` c ) ) -> b e. Y )
23 opelxpi 
 |-  ( ( a e. X /\ b e. Y ) -> <. a , b >. e. ( X X. Y ) )
24 21 22 23 syl2anc 
 |-  ( ( ( ( ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) /\ a e. X ) /\ ( F ` a ) = ( 1st ` c ) ) /\ b e. Y ) /\ ( G ` b ) = ( 2nd ` c ) ) -> <. a , b >. e. ( X X. Y ) )
25 simpllr 
 |-  ( ( ( ( ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) /\ a e. X ) /\ ( F ` a ) = ( 1st ` c ) ) /\ b e. Y ) /\ ( G ` b ) = ( 2nd ` c ) ) -> ( F ` a ) = ( 1st ` c ) )
26 simpr 
 |-  ( ( ( ( ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) /\ a e. X ) /\ ( F ` a ) = ( 1st ` c ) ) /\ b e. Y ) /\ ( G ` b ) = ( 2nd ` c ) ) -> ( G ` b ) = ( 2nd ` c ) )
27 25 26 opeq12d 
 |-  ( ( ( ( ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) /\ a e. X ) /\ ( F ` a ) = ( 1st ` c ) ) /\ b e. Y ) /\ ( G ` b ) = ( 2nd ` c ) ) -> <. ( F ` a ) , ( G ` b ) >. = <. ( 1st ` c ) , ( 2nd ` c ) >. )
28 4 ad5antr 
 |-  ( ( ( ( ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) /\ a e. X ) /\ ( F ` a ) = ( 1st ` c ) ) /\ b e. Y ) /\ ( G ` b ) = ( 2nd ` c ) ) -> X C_ A )
29 28 21 sseldd 
 |-  ( ( ( ( ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) /\ a e. X ) /\ ( F ` a ) = ( 1st ` c ) ) /\ b e. Y ) /\ ( G ` b ) = ( 2nd ` c ) ) -> a e. A )
30 5 ad5antr 
 |-  ( ( ( ( ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) /\ a e. X ) /\ ( F ` a ) = ( 1st ` c ) ) /\ b e. Y ) /\ ( G ` b ) = ( 2nd ` c ) ) -> Y C_ B )
31 30 22 sseldd 
 |-  ( ( ( ( ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) /\ a e. X ) /\ ( F ` a ) = ( 1st ` c ) ) /\ b e. Y ) /\ ( G ` b ) = ( 2nd ` c ) ) -> b e. B )
32 1 29 31 fvproj 
 |-  ( ( ( ( ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) /\ a e. X ) /\ ( F ` a ) = ( 1st ` c ) ) /\ b e. Y ) /\ ( G ` b ) = ( 2nd ` c ) ) -> ( H ` <. a , b >. ) = <. ( F ` a ) , ( G ` b ) >. )
33 1st2nd2 
 |-  ( c e. ( ( F " X ) X. ( G " Y ) ) -> c = <. ( 1st ` c ) , ( 2nd ` c ) >. )
34 33 ad5antlr 
 |-  ( ( ( ( ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) /\ a e. X ) /\ ( F ` a ) = ( 1st ` c ) ) /\ b e. Y ) /\ ( G ` b ) = ( 2nd ` c ) ) -> c = <. ( 1st ` c ) , ( 2nd ` c ) >. )
35 27 32 34 3eqtr4d 
 |-  ( ( ( ( ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) /\ a e. X ) /\ ( F ` a ) = ( 1st ` c ) ) /\ b e. Y ) /\ ( G ` b ) = ( 2nd ` c ) ) -> ( H ` <. a , b >. ) = c )
36 fveqeq2 
 |-  ( z = <. a , b >. -> ( ( H ` z ) = c <-> ( H ` <. a , b >. ) = c ) )
37 36 rspcev 
 |-  ( ( <. a , b >. e. ( X X. Y ) /\ ( H ` <. a , b >. ) = c ) -> E. z e. ( X X. Y ) ( H ` z ) = c )
38 24 35 37 syl2anc 
 |-  ( ( ( ( ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) /\ a e. X ) /\ ( F ` a ) = ( 1st ` c ) ) /\ b e. Y ) /\ ( G ` b ) = ( 2nd ` c ) ) -> E. z e. ( X X. Y ) ( H ` z ) = c )
39 3 ad3antrrr 
 |-  ( ( ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) /\ a e. X ) /\ ( F ` a ) = ( 1st ` c ) ) -> G Fn B )
40 fnfun 
 |-  ( G Fn B -> Fun G )
41 39 40 syl 
 |-  ( ( ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) /\ a e. X ) /\ ( F ` a ) = ( 1st ` c ) ) -> Fun G )
42 xp2nd 
 |-  ( c e. ( ( F " X ) X. ( G " Y ) ) -> ( 2nd ` c ) e. ( G " Y ) )
43 42 ad3antlr 
 |-  ( ( ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) /\ a e. X ) /\ ( F ` a ) = ( 1st ` c ) ) -> ( 2nd ` c ) e. ( G " Y ) )
44 fvelima 
 |-  ( ( Fun G /\ ( 2nd ` c ) e. ( G " Y ) ) -> E. b e. Y ( G ` b ) = ( 2nd ` c ) )
45 41 43 44 syl2anc 
 |-  ( ( ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) /\ a e. X ) /\ ( F ` a ) = ( 1st ` c ) ) -> E. b e. Y ( G ` b ) = ( 2nd ` c ) )
46 38 45 r19.29a 
 |-  ( ( ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) /\ a e. X ) /\ ( F ` a ) = ( 1st ` c ) ) -> E. z e. ( X X. Y ) ( H ` z ) = c )
47 2 adantr 
 |-  ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) -> F Fn A )
48 fnfun 
 |-  ( F Fn A -> Fun F )
49 47 48 syl 
 |-  ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) -> Fun F )
50 xp1st 
 |-  ( c e. ( ( F " X ) X. ( G " Y ) ) -> ( 1st ` c ) e. ( F " X ) )
51 50 adantl 
 |-  ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) -> ( 1st ` c ) e. ( F " X ) )
52 fvelima 
 |-  ( ( Fun F /\ ( 1st ` c ) e. ( F " X ) ) -> E. a e. X ( F ` a ) = ( 1st ` c ) )
53 49 51 52 syl2anc 
 |-  ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) -> E. a e. X ( F ` a ) = ( 1st ` c ) )
54 46 53 r19.29a 
 |-  ( ( ph /\ c e. ( ( F " X ) X. ( G " Y ) ) ) -> E. z e. ( X X. Y ) ( H ` z ) = c )
55 simpr 
 |-  ( ( ( ph /\ z e. ( X X. Y ) ) /\ ( H ` z ) = c ) -> ( H ` z ) = c )
56 18 ad2antrr 
 |-  ( ( ( ph /\ z e. ( X X. Y ) ) /\ ( H ` z ) = c ) -> ( X X. Y ) C_ ( A X. B ) )
57 simplr 
 |-  ( ( ( ph /\ z e. ( X X. Y ) ) /\ ( H ` z ) = c ) -> z e. ( X X. Y ) )
58 56 57 sseldd 
 |-  ( ( ( ph /\ z e. ( X X. Y ) ) /\ ( H ` z ) = c ) -> z e. ( A X. B ) )
59 15 fvmpt2 
 |-  ( ( z e. ( A X. B ) /\ <. ( F ` ( 1st ` z ) ) , ( G ` ( 2nd ` z ) ) >. e. _V ) -> ( H ` z ) = <. ( F ` ( 1st ` z ) ) , ( G ` ( 2nd ` z ) ) >. )
60 58 6 59 sylancl 
 |-  ( ( ( ph /\ z e. ( X X. Y ) ) /\ ( H ` z ) = c ) -> ( H ` z ) = <. ( F ` ( 1st ` z ) ) , ( G ` ( 2nd ` z ) ) >. )
61 2 ad2antrr 
 |-  ( ( ( ph /\ z e. ( X X. Y ) ) /\ ( H ` z ) = c ) -> F Fn A )
62 4 ad2antrr 
 |-  ( ( ( ph /\ z e. ( X X. Y ) ) /\ ( H ` z ) = c ) -> X C_ A )
63 xp1st 
 |-  ( z e. ( X X. Y ) -> ( 1st ` z ) e. X )
64 57 63 syl 
 |-  ( ( ( ph /\ z e. ( X X. Y ) ) /\ ( H ` z ) = c ) -> ( 1st ` z ) e. X )
65 fnfvima 
 |-  ( ( F Fn A /\ X C_ A /\ ( 1st ` z ) e. X ) -> ( F ` ( 1st ` z ) ) e. ( F " X ) )
66 61 62 64 65 syl3anc 
 |-  ( ( ( ph /\ z e. ( X X. Y ) ) /\ ( H ` z ) = c ) -> ( F ` ( 1st ` z ) ) e. ( F " X ) )
67 3 ad2antrr 
 |-  ( ( ( ph /\ z e. ( X X. Y ) ) /\ ( H ` z ) = c ) -> G Fn B )
68 5 ad2antrr 
 |-  ( ( ( ph /\ z e. ( X X. Y ) ) /\ ( H ` z ) = c ) -> Y C_ B )
69 xp2nd 
 |-  ( z e. ( X X. Y ) -> ( 2nd ` z ) e. Y )
70 57 69 syl 
 |-  ( ( ( ph /\ z e. ( X X. Y ) ) /\ ( H ` z ) = c ) -> ( 2nd ` z ) e. Y )
71 fnfvima 
 |-  ( ( G Fn B /\ Y C_ B /\ ( 2nd ` z ) e. Y ) -> ( G ` ( 2nd ` z ) ) e. ( G " Y ) )
72 67 68 70 71 syl3anc 
 |-  ( ( ( ph /\ z e. ( X X. Y ) ) /\ ( H ` z ) = c ) -> ( G ` ( 2nd ` z ) ) e. ( G " Y ) )
73 opelxpi 
 |-  ( ( ( F ` ( 1st ` z ) ) e. ( F " X ) /\ ( G ` ( 2nd ` z ) ) e. ( G " Y ) ) -> <. ( F ` ( 1st ` z ) ) , ( G ` ( 2nd ` z ) ) >. e. ( ( F " X ) X. ( G " Y ) ) )
74 66 72 73 syl2anc 
 |-  ( ( ( ph /\ z e. ( X X. Y ) ) /\ ( H ` z ) = c ) -> <. ( F ` ( 1st ` z ) ) , ( G ` ( 2nd ` z ) ) >. e. ( ( F " X ) X. ( G " Y ) ) )
75 60 74 eqeltrd 
 |-  ( ( ( ph /\ z e. ( X X. Y ) ) /\ ( H ` z ) = c ) -> ( H ` z ) e. ( ( F " X ) X. ( G " Y ) ) )
76 55 75 eqeltrrd 
 |-  ( ( ( ph /\ z e. ( X X. Y ) ) /\ ( H ` z ) = c ) -> c e. ( ( F " X ) X. ( G " Y ) ) )
77 76 r19.29an 
 |-  ( ( ph /\ E. z e. ( X X. Y ) ( H ` z ) = c ) -> c e. ( ( F " X ) X. ( G " Y ) ) )
78 54 77 impbida 
 |-  ( ph -> ( c e. ( ( F " X ) X. ( G " Y ) ) <-> E. z e. ( X X. Y ) ( H ` z ) = c ) )
79 20 78 bitr4d 
 |-  ( ph -> ( c e. ( H " ( X X. Y ) ) <-> c e. ( ( F " X ) X. ( G " Y ) ) ) )
80 79 eqrdv 
 |-  ( ph -> ( H " ( X X. Y ) ) = ( ( F " X ) X. ( G " Y ) ) )