Metamath Proof Explorer

Theorem fmucndlem

Description: Lemma for fmucnd . (Contributed by Thierry Arnoux, 19-Nov-2017)

Ref Expression
Assertion fmucndlem 
|- ( ( F Fn X /\ A C_ X ) -> ( ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " ( A X. A ) ) = ( ( F " A ) X. ( F " A ) ) )

Proof

Step Hyp Ref Expression
1 df-ima 
 |-  ( ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " ( A X. A ) ) = ran ( ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) |` ( A X. A ) )
2 simpr 
 |-  ( ( F Fn X /\ A C_ X ) -> A C_ X )
3 resmpo 
 |-  ( ( A C_ X /\ A C_ X ) -> ( ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) |` ( A X. A ) ) = ( x e. A , y e. A |-> <. ( F ` x ) , ( F ` y ) >. ) )
4 2 3 sylancom 
 |-  ( ( F Fn X /\ A C_ X ) -> ( ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) |` ( A X. A ) ) = ( x e. A , y e. A |-> <. ( F ` x ) , ( F ` y ) >. ) )
5 4 rneqd 
 |-  ( ( F Fn X /\ A C_ X ) -> ran ( ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) |` ( A X. A ) ) = ran ( x e. A , y e. A |-> <. ( F ` x ) , ( F ` y ) >. ) )
6 1 5 eqtrid 
 |-  ( ( F Fn X /\ A C_ X ) -> ( ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " ( A X. A ) ) = ran ( x e. A , y e. A |-> <. ( F ` x ) , ( F ` y ) >. ) )
7 vex 
 |-  x e. _V
8 vex 
 |-  y e. _V
9 7 8 op1std 
 |-  ( p = <. x , y >. -> ( 1st ` p ) = x )
10 9 fveq2d 
 |-  ( p = <. x , y >. -> ( F ` ( 1st ` p ) ) = ( F ` x ) )
11 7 8 op2ndd 
 |-  ( p = <. x , y >. -> ( 2nd ` p ) = y )
12 11 fveq2d 
 |-  ( p = <. x , y >. -> ( F ` ( 2nd ` p ) ) = ( F ` y ) )
13 10 12 opeq12d 
 |-  ( p = <. x , y >. -> <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. = <. ( F ` x ) , ( F ` y ) >. )
14 13 mpompt 
 |-  ( p e. ( A X. A ) |-> <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. ) = ( x e. A , y e. A |-> <. ( F ` x ) , ( F ` y ) >. )
15 14 eqcomi 
 |-  ( x e. A , y e. A |-> <. ( F ` x ) , ( F ` y ) >. ) = ( p e. ( A X. A ) |-> <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. )
16 15 rneqi 
 |-  ran ( x e. A , y e. A |-> <. ( F ` x ) , ( F ` y ) >. ) = ran ( p e. ( A X. A ) |-> <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. )
17 fvexd 
 |-  ( ( T. /\ p e. ( A X. A ) ) -> ( F ` ( 1st ` p ) ) e. _V )
18 fvexd 
 |-  ( ( T. /\ p e. ( A X. A ) ) -> ( F ` ( 2nd ` p ) ) e. _V )
19 16 17 18 fliftrel 
 |-  ( T. -> ran ( x e. A , y e. A |-> <. ( F ` x ) , ( F ` y ) >. ) C_ ( _V X. _V ) )
20 19 mptru 
 |-  ran ( x e. A , y e. A |-> <. ( F ` x ) , ( F ` y ) >. ) C_ ( _V X. _V )
21 20 sseli 
 |-  ( p e. ran ( x e. A , y e. A |-> <. ( F ` x ) , ( F ` y ) >. ) -> p e. ( _V X. _V ) )
22 21 adantl 
 |-  ( ( ( F Fn X /\ A C_ X ) /\ p e. ran ( x e. A , y e. A |-> <. ( F ` x ) , ( F ` y ) >. ) ) -> p e. ( _V X. _V ) )
23 xpss 
 |-  ( ( F " A ) X. ( F " A ) ) C_ ( _V X. _V )
24 23 sseli 
 |-  ( p e. ( ( F " A ) X. ( F " A ) ) -> p e. ( _V X. _V ) )
25 24 adantl 
 |-  ( ( ( F Fn X /\ A C_ X ) /\ p e. ( ( F " A ) X. ( F " A ) ) ) -> p e. ( _V X. _V ) )
26 eqid 
 |-  ( x e. A , y e. A |-> <. ( F ` x ) , ( F ` y ) >. ) = ( x e. A , y e. A |-> <. ( F ` x ) , ( F ` y ) >. )
27 opex 
 |-  <. ( F ` x ) , ( F ` y ) >. e. _V
28 26 27 elrnmpo 
 |-  ( <. ( 1st ` p ) , ( 2nd ` p ) >. e. ran ( x e. A , y e. A |-> <. ( F ` x ) , ( F ` y ) >. ) <-> E. x e. A E. y e. A <. ( 1st ` p ) , ( 2nd ` p ) >. = <. ( F ` x ) , ( F ` y ) >. )
29 eqcom 
 |-  ( <. ( 1st ` p ) , ( 2nd ` p ) >. = <. ( F ` x ) , ( F ` y ) >. <-> <. ( F ` x ) , ( F ` y ) >. = <. ( 1st ` p ) , ( 2nd ` p ) >. )
30 fvex 
 |-  ( 1st ` p ) e. _V
31 fvex 
 |-  ( 2nd ` p ) e. _V
32 30 31 opth2 
 |-  ( <. ( F ` x ) , ( F ` y ) >. = <. ( 1st ` p ) , ( 2nd ` p ) >. <-> ( ( F ` x ) = ( 1st ` p ) /\ ( F ` y ) = ( 2nd ` p ) ) )
33 29 32 bitri 
 |-  ( <. ( 1st ` p ) , ( 2nd ` p ) >. = <. ( F ` x ) , ( F ` y ) >. <-> ( ( F ` x ) = ( 1st ` p ) /\ ( F ` y ) = ( 2nd ` p ) ) )
34 33 2rexbii 
 |-  ( E. x e. A E. y e. A <. ( 1st ` p ) , ( 2nd ` p ) >. = <. ( F ` x ) , ( F ` y ) >. <-> E. x e. A E. y e. A ( ( F ` x ) = ( 1st ` p ) /\ ( F ` y ) = ( 2nd ` p ) ) )
35 reeanv 
 |-  ( E. x e. A E. y e. A ( ( F ` x ) = ( 1st ` p ) /\ ( F ` y ) = ( 2nd ` p ) ) <-> ( E. x e. A ( F ` x ) = ( 1st ` p ) /\ E. y e. A ( F ` y ) = ( 2nd ` p ) ) )
36 28 34 35 3bitri 
 |-  ( <. ( 1st ` p ) , ( 2nd ` p ) >. e. ran ( x e. A , y e. A |-> <. ( F ` x ) , ( F ` y ) >. ) <-> ( E. x e. A ( F ` x ) = ( 1st ` p ) /\ E. y e. A ( F ` y ) = ( 2nd ` p ) ) )
37 fvelimab 
 |-  ( ( F Fn X /\ A C_ X ) -> ( ( 1st ` p ) e. ( F " A ) <-> E. x e. A ( F ` x ) = ( 1st ` p ) ) )
38 fvelimab 
 |-  ( ( F Fn X /\ A C_ X ) -> ( ( 2nd ` p ) e. ( F " A ) <-> E. y e. A ( F ` y ) = ( 2nd ` p ) ) )
39 37 38 anbi12d 
 |-  ( ( F Fn X /\ A C_ X ) -> ( ( ( 1st ` p ) e. ( F " A ) /\ ( 2nd ` p ) e. ( F " A ) ) <-> ( E. x e. A ( F ` x ) = ( 1st ` p ) /\ E. y e. A ( F ` y ) = ( 2nd ` p ) ) ) )
40 36 39 bitr4id 
 |-  ( ( F Fn X /\ A C_ X ) -> ( <. ( 1st ` p ) , ( 2nd ` p ) >. e. ran ( x e. A , y e. A |-> <. ( F ` x ) , ( F ` y ) >. ) <-> ( ( 1st ` p ) e. ( F " A ) /\ ( 2nd ` p ) e. ( F " A ) ) ) )
41 opelxp 
 |-  ( <. ( 1st ` p ) , ( 2nd ` p ) >. e. ( ( F " A ) X. ( F " A ) ) <-> ( ( 1st ` p ) e. ( F " A ) /\ ( 2nd ` p ) e. ( F " A ) ) )
42 40 41 bitr4di 
 |-  ( ( F Fn X /\ A C_ X ) -> ( <. ( 1st ` p ) , ( 2nd ` p ) >. e. ran ( x e. A , y e. A |-> <. ( F ` x ) , ( F ` y ) >. ) <-> <. ( 1st ` p ) , ( 2nd ` p ) >. e. ( ( F " A ) X. ( F " A ) ) ) )
43 42 adantr 
 |-  ( ( ( F Fn X /\ A C_ X ) /\ p e. ( _V X. _V ) ) -> ( <. ( 1st ` p ) , ( 2nd ` p ) >. e. ran ( x e. A , y e. A |-> <. ( F ` x ) , ( F ` y ) >. ) <-> <. ( 1st ` p ) , ( 2nd ` p ) >. e. ( ( F " A ) X. ( F " A ) ) ) )
44 1st2nd2 
 |-  ( p e. ( _V X. _V ) -> p = <. ( 1st ` p ) , ( 2nd ` p ) >. )
45 44 adantl 
 |-  ( ( ( F Fn X /\ A C_ X ) /\ p e. ( _V X. _V ) ) -> p = <. ( 1st ` p ) , ( 2nd ` p ) >. )
46 45 eleq1d 
 |-  ( ( ( F Fn X /\ A C_ X ) /\ p e. ( _V X. _V ) ) -> ( p e. ran ( x e. A , y e. A |-> <. ( F ` x ) , ( F ` y ) >. ) <-> <. ( 1st ` p ) , ( 2nd ` p ) >. e. ran ( x e. A , y e. A |-> <. ( F ` x ) , ( F ` y ) >. ) ) )
47 45 eleq1d 
 |-  ( ( ( F Fn X /\ A C_ X ) /\ p e. ( _V X. _V ) ) -> ( p e. ( ( F " A ) X. ( F " A ) ) <-> <. ( 1st ` p ) , ( 2nd ` p ) >. e. ( ( F " A ) X. ( F " A ) ) ) )
48 43 46 47 3bitr4d 
 |-  ( ( ( F Fn X /\ A C_ X ) /\ p e. ( _V X. _V ) ) -> ( p e. ran ( x e. A , y e. A |-> <. ( F ` x ) , ( F ` y ) >. ) <-> p e. ( ( F " A ) X. ( F " A ) ) ) )
49 22 25 48 eqrdav 
 |-  ( ( F Fn X /\ A C_ X ) -> ran ( x e. A , y e. A |-> <. ( F ` x ) , ( F ` y ) >. ) = ( ( F " A ) X. ( F " A ) ) )
50 6 49 eqtrd 
 |-  ( ( F Fn X /\ A C_ X ) -> ( ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " ( A X. A ) ) = ( ( F " A ) X. ( F " A ) ) )