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