Metamath Proof Explorer

Theorem 2arymaptf1

Description: The mapping of binary (endo)functions is a one-to-one function into the set of binary operations. (Contributed by AV, 22-May-2024)

Ref Expression
Hypothesis 2arymaptf.h 
|- H = ( h e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) )
Assertion 2arymaptf1 
|- ( X e. V -> H : ( 2 -aryF X ) -1-1-> ( X ^m ( X X. X ) ) )

Proof

Step Hyp Ref Expression
1 2arymaptf.h 
 |-  H = ( h e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) )
2 1 2arymaptf 
 |-  ( X e. V -> H : ( 2 -aryF X ) --> ( X ^m ( X X. X ) ) )
3 1 2arymaptfv 
 |-  ( f e. ( 2 -aryF X ) -> ( H ` f ) = ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) )
4 3 ad2antrl 
 |-  ( ( X e. V /\ ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) ) -> ( H ` f ) = ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) )
5 1 2arymaptfv 
 |-  ( g e. ( 2 -aryF X ) -> ( H ` g ) = ( x e. X , y e. X |-> ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) )
6 5 ad2antll 
 |-  ( ( X e. V /\ ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) ) -> ( H ` g ) = ( x e. X , y e. X |-> ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) )
7 4 6 eqeq12d 
 |-  ( ( X e. V /\ ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) ) -> ( ( H ` f ) = ( H ` g ) <-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) = ( x e. X , y e. X |-> ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) ) )
8 fvex 
 |-  ( f ` { <. 0 , x >. , <. 1 , y >. } ) e. _V
9 8 rgen2w 
 |-  A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) e. _V
10 mpo2eqb 
 |-  ( A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) e. _V -> ( ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) = ( x e. X , y e. X |-> ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) <-> A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) )
11 9 10 mp1i 
 |-  ( ( X e. V /\ ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) ) -> ( ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) = ( x e. X , y e. X |-> ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) <-> A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) )
12 2aryfvalel 
 |-  ( X e. V -> ( f e. ( 2 -aryF X ) <-> f : ( X ^m { 0 , 1 } ) --> X ) )
13 2aryfvalel 
 |-  ( X e. V -> ( g e. ( 2 -aryF X ) <-> g : ( X ^m { 0 , 1 } ) --> X ) )
14 12 13 anbi12d 
 |-  ( X e. V -> ( ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) <-> ( f : ( X ^m { 0 , 1 } ) --> X /\ g : ( X ^m { 0 , 1 } ) --> X ) ) )
15 ffn 
 |-  ( f : ( X ^m { 0 , 1 } ) --> X -> f Fn ( X ^m { 0 , 1 } ) )
16 15 adantr 
 |-  ( ( f : ( X ^m { 0 , 1 } ) --> X /\ g : ( X ^m { 0 , 1 } ) --> X ) -> f Fn ( X ^m { 0 , 1 } ) )
17 16 3ad2ant2 
 |-  ( ( X e. V /\ ( f : ( X ^m { 0 , 1 } ) --> X /\ g : ( X ^m { 0 , 1 } ) --> X ) /\ A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) -> f Fn ( X ^m { 0 , 1 } ) )
18 ffn 
 |-  ( g : ( X ^m { 0 , 1 } ) --> X -> g Fn ( X ^m { 0 , 1 } ) )
19 18 adantl 
 |-  ( ( f : ( X ^m { 0 , 1 } ) --> X /\ g : ( X ^m { 0 , 1 } ) --> X ) -> g Fn ( X ^m { 0 , 1 } ) )
20 19 3ad2ant2 
 |-  ( ( X e. V /\ ( f : ( X ^m { 0 , 1 } ) --> X /\ g : ( X ^m { 0 , 1 } ) --> X ) /\ A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) -> g Fn ( X ^m { 0 , 1 } ) )
21 elmapi 
 |-  ( z e. ( X ^m { 0 , 1 } ) -> z : { 0 , 1 } --> X )
22 0ne1 
 |-  0 =/= 1
23 c0ex 
 |-  0 e. _V
24 1ex 
 |-  1 e. _V
25 23 24 fprb 
 |-  ( 0 =/= 1 -> ( z : { 0 , 1 } --> X <-> E. a e. X E. b e. X z = { <. 0 , a >. , <. 1 , b >. } ) )
26 22 25 ax-mp 
 |-  ( z : { 0 , 1 } --> X <-> E. a e. X E. b e. X z = { <. 0 , a >. , <. 1 , b >. } )
27 21 26 sylib 
 |-  ( z e. ( X ^m { 0 , 1 } ) -> E. a e. X E. b e. X z = { <. 0 , a >. , <. 1 , b >. } )
28 opeq2 
 |-  ( x = a -> <. 0 , x >. = <. 0 , a >. )
29 28 preq1d 
 |-  ( x = a -> { <. 0 , x >. , <. 1 , y >. } = { <. 0 , a >. , <. 1 , y >. } )
30 29 fveq2d 
 |-  ( x = a -> ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( f ` { <. 0 , a >. , <. 1 , y >. } ) )
31 29 fveq2d 
 |-  ( x = a -> ( g ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , a >. , <. 1 , y >. } ) )
32 30 31 eqeq12d 
 |-  ( x = a -> ( ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) <-> ( f ` { <. 0 , a >. , <. 1 , y >. } ) = ( g ` { <. 0 , a >. , <. 1 , y >. } ) ) )
33 opeq2 
 |-  ( y = b -> <. 1 , y >. = <. 1 , b >. )
34 33 preq2d 
 |-  ( y = b -> { <. 0 , a >. , <. 1 , y >. } = { <. 0 , a >. , <. 1 , b >. } )
35 34 fveq2d 
 |-  ( y = b -> ( f ` { <. 0 , a >. , <. 1 , y >. } ) = ( f ` { <. 0 , a >. , <. 1 , b >. } ) )
36 34 fveq2d 
 |-  ( y = b -> ( g ` { <. 0 , a >. , <. 1 , y >. } ) = ( g ` { <. 0 , a >. , <. 1 , b >. } ) )
37 35 36 eqeq12d 
 |-  ( y = b -> ( ( f ` { <. 0 , a >. , <. 1 , y >. } ) = ( g ` { <. 0 , a >. , <. 1 , y >. } ) <-> ( f ` { <. 0 , a >. , <. 1 , b >. } ) = ( g ` { <. 0 , a >. , <. 1 , b >. } ) ) )
38 32 37 rspc2va 
 |-  ( ( ( a e. X /\ b e. X ) /\ A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) -> ( f ` { <. 0 , a >. , <. 1 , b >. } ) = ( g ` { <. 0 , a >. , <. 1 , b >. } ) )
39 38 expcom 
 |-  ( A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) -> ( ( a e. X /\ b e. X ) -> ( f ` { <. 0 , a >. , <. 1 , b >. } ) = ( g ` { <. 0 , a >. , <. 1 , b >. } ) ) )
40 39 3ad2ant3 
 |-  ( ( X e. V /\ ( f : ( X ^m { 0 , 1 } ) --> X /\ g : ( X ^m { 0 , 1 } ) --> X ) /\ A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) -> ( ( a e. X /\ b e. X ) -> ( f ` { <. 0 , a >. , <. 1 , b >. } ) = ( g ` { <. 0 , a >. , <. 1 , b >. } ) ) )
41 40 com12 
 |-  ( ( a e. X /\ b e. X ) -> ( ( X e. V /\ ( f : ( X ^m { 0 , 1 } ) --> X /\ g : ( X ^m { 0 , 1 } ) --> X ) /\ A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) -> ( f ` { <. 0 , a >. , <. 1 , b >. } ) = ( g ` { <. 0 , a >. , <. 1 , b >. } ) ) )
42 41 adantr 
 |-  ( ( ( a e. X /\ b e. X ) /\ z = { <. 0 , a >. , <. 1 , b >. } ) -> ( ( X e. V /\ ( f : ( X ^m { 0 , 1 } ) --> X /\ g : ( X ^m { 0 , 1 } ) --> X ) /\ A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) -> ( f ` { <. 0 , a >. , <. 1 , b >. } ) = ( g ` { <. 0 , a >. , <. 1 , b >. } ) ) )
43 fveq2 
 |-  ( z = { <. 0 , a >. , <. 1 , b >. } -> ( f ` z ) = ( f ` { <. 0 , a >. , <. 1 , b >. } ) )
44 fveq2 
 |-  ( z = { <. 0 , a >. , <. 1 , b >. } -> ( g ` z ) = ( g ` { <. 0 , a >. , <. 1 , b >. } ) )
45 43 44 eqeq12d 
 |-  ( z = { <. 0 , a >. , <. 1 , b >. } -> ( ( f ` z ) = ( g ` z ) <-> ( f ` { <. 0 , a >. , <. 1 , b >. } ) = ( g ` { <. 0 , a >. , <. 1 , b >. } ) ) )
46 45 adantl 
 |-  ( ( ( a e. X /\ b e. X ) /\ z = { <. 0 , a >. , <. 1 , b >. } ) -> ( ( f ` z ) = ( g ` z ) <-> ( f ` { <. 0 , a >. , <. 1 , b >. } ) = ( g ` { <. 0 , a >. , <. 1 , b >. } ) ) )
47 42 46 sylibrd 
 |-  ( ( ( a e. X /\ b e. X ) /\ z = { <. 0 , a >. , <. 1 , b >. } ) -> ( ( X e. V /\ ( f : ( X ^m { 0 , 1 } ) --> X /\ g : ( X ^m { 0 , 1 } ) --> X ) /\ A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) -> ( f ` z ) = ( g ` z ) ) )
48 47 ex 
 |-  ( ( a e. X /\ b e. X ) -> ( z = { <. 0 , a >. , <. 1 , b >. } -> ( ( X e. V /\ ( f : ( X ^m { 0 , 1 } ) --> X /\ g : ( X ^m { 0 , 1 } ) --> X ) /\ A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) -> ( f ` z ) = ( g ` z ) ) ) )
49 48 rexlimivv 
 |-  ( E. a e. X E. b e. X z = { <. 0 , a >. , <. 1 , b >. } -> ( ( X e. V /\ ( f : ( X ^m { 0 , 1 } ) --> X /\ g : ( X ^m { 0 , 1 } ) --> X ) /\ A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) -> ( f ` z ) = ( g ` z ) ) )
50 27 49 syl 
 |-  ( z e. ( X ^m { 0 , 1 } ) -> ( ( X e. V /\ ( f : ( X ^m { 0 , 1 } ) --> X /\ g : ( X ^m { 0 , 1 } ) --> X ) /\ A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) -> ( f ` z ) = ( g ` z ) ) )
51 50 impcom 
 |-  ( ( ( X e. V /\ ( f : ( X ^m { 0 , 1 } ) --> X /\ g : ( X ^m { 0 , 1 } ) --> X ) /\ A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) /\ z e. ( X ^m { 0 , 1 } ) ) -> ( f ` z ) = ( g ` z ) )
52 17 20 51 eqfnfvd 
 |-  ( ( X e. V /\ ( f : ( X ^m { 0 , 1 } ) --> X /\ g : ( X ^m { 0 , 1 } ) --> X ) /\ A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) -> f = g )
53 52 3exp 
 |-  ( X e. V -> ( ( f : ( X ^m { 0 , 1 } ) --> X /\ g : ( X ^m { 0 , 1 } ) --> X ) -> ( A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) -> f = g ) ) )
54 14 53 sylbid 
 |-  ( X e. V -> ( ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) -> ( A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) -> f = g ) ) )
55 54 imp 
 |-  ( ( X e. V /\ ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) ) -> ( A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) -> f = g ) )
56 11 55 sylbid 
 |-  ( ( X e. V /\ ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) ) -> ( ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) = ( x e. X , y e. X |-> ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) -> f = g ) )
57 7 56 sylbid 
 |-  ( ( X e. V /\ ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) ) -> ( ( H ` f ) = ( H ` g ) -> f = g ) )
58 57 ralrimivva 
 |-  ( X e. V -> A. f e. ( 2 -aryF X ) A. g e. ( 2 -aryF X ) ( ( H ` f ) = ( H ` g ) -> f = g ) )
59 dff13 
 |-  ( H : ( 2 -aryF X ) -1-1-> ( X ^m ( X X. X ) ) <-> ( H : ( 2 -aryF X ) --> ( X ^m ( X X. X ) ) /\ A. f e. ( 2 -aryF X ) A. g e. ( 2 -aryF X ) ( ( H ` f ) = ( H ` g ) -> f = g ) ) )
60 2 58 59 sylanbrc 
 |-  ( X e. V -> H : ( 2 -aryF X ) -1-1-> ( X ^m ( X X. X ) ) )