Metamath Proof Explorer

Theorem 2arymaptfo

Description: The mapping of binary (endo)functions is a function onto the set of binary operations. (Contributed by AV, 23-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 2arymaptfo 
|- ( X e. V -> H : ( 2 -aryF X ) -onto-> ( 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 elmapi 
 |-  ( f e. ( X ^m ( X X. X ) ) -> f : ( X X. X ) --> X )
4 eqid 
 |-  ( a e. ( X ^m { 0 , 1 } ) |-> ( ( a ` 0 ) f ( a ` 1 ) ) ) = ( a e. ( X ^m { 0 , 1 } ) |-> ( ( a ` 0 ) f ( a ` 1 ) ) )
5 4 2arympt 
 |-  ( ( X e. V /\ f : ( X X. X ) --> X ) -> ( a e. ( X ^m { 0 , 1 } ) |-> ( ( a ` 0 ) f ( a ` 1 ) ) ) e. ( 2 -aryF X ) )
6 3 5 sylan2 
 |-  ( ( X e. V /\ f e. ( X ^m ( X X. X ) ) ) -> ( a e. ( X ^m { 0 , 1 } ) |-> ( ( a ` 0 ) f ( a ` 1 ) ) ) e. ( 2 -aryF X ) )
7 fveq2 
 |-  ( g = ( a e. ( X ^m { 0 , 1 } ) |-> ( ( a ` 0 ) f ( a ` 1 ) ) ) -> ( H ` g ) = ( H ` ( a e. ( X ^m { 0 , 1 } ) |-> ( ( a ` 0 ) f ( a ` 1 ) ) ) ) )
8 7 eqeq2d 
 |-  ( g = ( a e. ( X ^m { 0 , 1 } ) |-> ( ( a ` 0 ) f ( a ` 1 ) ) ) -> ( f = ( H ` g ) <-> f = ( H ` ( a e. ( X ^m { 0 , 1 } ) |-> ( ( a ` 0 ) f ( a ` 1 ) ) ) ) ) )
9 8 adantl 
 |-  ( ( ( X e. V /\ f e. ( X ^m ( X X. X ) ) ) /\ g = ( a e. ( X ^m { 0 , 1 } ) |-> ( ( a ` 0 ) f ( a ` 1 ) ) ) ) -> ( f = ( H ` g ) <-> f = ( H ` ( a e. ( X ^m { 0 , 1 } ) |-> ( ( a ` 0 ) f ( a ` 1 ) ) ) ) ) )
10 elmapfn 
 |-  ( f e. ( X ^m ( X X. X ) ) -> f Fn ( X X. X ) )
11 10 adantl 
 |-  ( ( X e. V /\ f e. ( X ^m ( X X. X ) ) ) -> f Fn ( X X. X ) )
12 fnov 
 |-  ( f Fn ( X X. X ) <-> f = ( x e. X , y e. X |-> ( x f y ) ) )
13 11 12 sylib 
 |-  ( ( X e. V /\ f e. ( X ^m ( X X. X ) ) ) -> f = ( x e. X , y e. X |-> ( x f y ) ) )
14 simp1r 
 |-  ( ( ( ( X e. V /\ f e. ( X ^m ( X X. X ) ) ) /\ h = ( a e. ( X ^m { 0 , 1 } ) |-> ( ( a ` 0 ) f ( a ` 1 ) ) ) ) /\ x e. X /\ y e. X ) -> h = ( a e. ( X ^m { 0 , 1 } ) |-> ( ( a ` 0 ) f ( a ` 1 ) ) ) )
15 fveq1 
 |-  ( a = { <. 0 , x >. , <. 1 , y >. } -> ( a ` 0 ) = ( { <. 0 , x >. , <. 1 , y >. } ` 0 ) )
16 0ne1 
 |-  0 =/= 1
17 c0ex 
 |-  0 e. _V
18 vex 
 |-  x e. _V
19 17 18 fvpr1 
 |-  ( 0 =/= 1 -> ( { <. 0 , x >. , <. 1 , y >. } ` 0 ) = x )
20 16 19 ax-mp 
 |-  ( { <. 0 , x >. , <. 1 , y >. } ` 0 ) = x
21 15 20 eqtrdi 
 |-  ( a = { <. 0 , x >. , <. 1 , y >. } -> ( a ` 0 ) = x )
22 fveq1 
 |-  ( a = { <. 0 , x >. , <. 1 , y >. } -> ( a ` 1 ) = ( { <. 0 , x >. , <. 1 , y >. } ` 1 ) )
23 1ex 
 |-  1 e. _V
24 vex 
 |-  y e. _V
25 23 24 fvpr2 
 |-  ( 0 =/= 1 -> ( { <. 0 , x >. , <. 1 , y >. } ` 1 ) = y )
26 16 25 ax-mp 
 |-  ( { <. 0 , x >. , <. 1 , y >. } ` 1 ) = y
27 22 26 eqtrdi 
 |-  ( a = { <. 0 , x >. , <. 1 , y >. } -> ( a ` 1 ) = y )
28 21 27 oveq12d 
 |-  ( a = { <. 0 , x >. , <. 1 , y >. } -> ( ( a ` 0 ) f ( a ` 1 ) ) = ( x f y ) )
29 28 adantl 
 |-  ( ( ( ( ( X e. V /\ f e. ( X ^m ( X X. X ) ) ) /\ h = ( a e. ( X ^m { 0 , 1 } ) |-> ( ( a ` 0 ) f ( a ` 1 ) ) ) ) /\ x e. X /\ y e. X ) /\ a = { <. 0 , x >. , <. 1 , y >. } ) -> ( ( a ` 0 ) f ( a ` 1 ) ) = ( x f y ) )
30 17 23 pm3.2i 
 |-  ( 0 e. _V /\ 1 e. _V )
31 fprg 
 |-  ( ( ( 0 e. _V /\ 1 e. _V ) /\ ( x e. X /\ y e. X ) /\ 0 =/= 1 ) -> { <. 0 , x >. , <. 1 , y >. } : { 0 , 1 } --> { x , y } )
32 30 16 31 mp3an13 
 |-  ( ( x e. X /\ y e. X ) -> { <. 0 , x >. , <. 1 , y >. } : { 0 , 1 } --> { x , y } )
33 32 3adant1 
 |-  ( ( X e. V /\ x e. X /\ y e. X ) -> { <. 0 , x >. , <. 1 , y >. } : { 0 , 1 } --> { x , y } )
34 prssi 
 |-  ( ( x e. X /\ y e. X ) -> { x , y } C_ X )
35 34 3adant1 
 |-  ( ( X e. V /\ x e. X /\ y e. X ) -> { x , y } C_ X )
36 33 35 fssd 
 |-  ( ( X e. V /\ x e. X /\ y e. X ) -> { <. 0 , x >. , <. 1 , y >. } : { 0 , 1 } --> X )
37 simp1 
 |-  ( ( X e. V /\ x e. X /\ y e. X ) -> X e. V )
38 prex 
 |-  { 0 , 1 } e. _V
39 38 a1i 
 |-  ( ( X e. V /\ x e. X /\ y e. X ) -> { 0 , 1 } e. _V )
40 37 39 elmapd 
 |-  ( ( X e. V /\ x e. X /\ y e. X ) -> ( { <. 0 , x >. , <. 1 , y >. } e. ( X ^m { 0 , 1 } ) <-> { <. 0 , x >. , <. 1 , y >. } : { 0 , 1 } --> X ) )
41 36 40 mpbird 
 |-  ( ( X e. V /\ x e. X /\ y e. X ) -> { <. 0 , x >. , <. 1 , y >. } e. ( X ^m { 0 , 1 } ) )
42 41 3adant1r 
 |-  ( ( ( X e. V /\ f e. ( X ^m ( X X. X ) ) ) /\ x e. X /\ y e. X ) -> { <. 0 , x >. , <. 1 , y >. } e. ( X ^m { 0 , 1 } ) )
43 42 3adant1r 
 |-  ( ( ( ( X e. V /\ f e. ( X ^m ( X X. X ) ) ) /\ h = ( a e. ( X ^m { 0 , 1 } ) |-> ( ( a ` 0 ) f ( a ` 1 ) ) ) ) /\ x e. X /\ y e. X ) -> { <. 0 , x >. , <. 1 , y >. } e. ( X ^m { 0 , 1 } ) )
44 ovexd 
 |-  ( ( ( ( X e. V /\ f e. ( X ^m ( X X. X ) ) ) /\ h = ( a e. ( X ^m { 0 , 1 } ) |-> ( ( a ` 0 ) f ( a ` 1 ) ) ) ) /\ x e. X /\ y e. X ) -> ( x f y ) e. _V )
45 nfv 
 |-  F/ a ( X e. V /\ f e. ( X ^m ( X X. X ) ) )
46 nfmpt1 
 |-  F/_ a ( a e. ( X ^m { 0 , 1 } ) |-> ( ( a ` 0 ) f ( a ` 1 ) ) )
47 46 nfeq2 
 |-  F/ a h = ( a e. ( X ^m { 0 , 1 } ) |-> ( ( a ` 0 ) f ( a ` 1 ) ) )
48 45 47 nfan 
 |-  F/ a ( ( X e. V /\ f e. ( X ^m ( X X. X ) ) ) /\ h = ( a e. ( X ^m { 0 , 1 } ) |-> ( ( a ` 0 ) f ( a ` 1 ) ) ) )
49 nfv 
 |-  F/ a x e. X
50 nfv 
 |-  F/ a y e. X
51 48 49 50 nf3an 
 |-  F/ a ( ( ( X e. V /\ f e. ( X ^m ( X X. X ) ) ) /\ h = ( a e. ( X ^m { 0 , 1 } ) |-> ( ( a ` 0 ) f ( a ` 1 ) ) ) ) /\ x e. X /\ y e. X )
52 nfcv 
 |-  F/_ a { <. 0 , x >. , <. 1 , y >. }
53 nfcv 
 |-  F/_ a ( x f y )
54 14 29 43 44 51 52 53 fvmptdf 
 |-  ( ( ( ( X e. V /\ f e. ( X ^m ( X X. X ) ) ) /\ h = ( a e. ( X ^m { 0 , 1 } ) |-> ( ( a ` 0 ) f ( a ` 1 ) ) ) ) /\ x e. X /\ y e. X ) -> ( h ` { <. 0 , x >. , <. 1 , y >. } ) = ( x f y ) )
55 54 mpoeq3dva 
 |-  ( ( ( X e. V /\ f e. ( X ^m ( X X. X ) ) ) /\ h = ( a e. ( X ^m { 0 , 1 } ) |-> ( ( a ` 0 ) f ( a ` 1 ) ) ) ) -> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) = ( x e. X , y e. X |-> ( x f y ) ) )
56 mpoexga 
 |-  ( ( X e. V /\ X e. V ) -> ( x e. X , y e. X |-> ( x f y ) ) e. _V )
57 56 anidms 
 |-  ( X e. V -> ( x e. X , y e. X |-> ( x f y ) ) e. _V )
58 57 adantr 
 |-  ( ( X e. V /\ f e. ( X ^m ( X X. X ) ) ) -> ( x e. X , y e. X |-> ( x f y ) ) e. _V )
59 1 55 6 58 fvmptd2 
 |-  ( ( X e. V /\ f e. ( X ^m ( X X. X ) ) ) -> ( H ` ( a e. ( X ^m { 0 , 1 } ) |-> ( ( a ` 0 ) f ( a ` 1 ) ) ) ) = ( x e. X , y e. X |-> ( x f y ) ) )
60 13 59 eqtr4d 
 |-  ( ( X e. V /\ f e. ( X ^m ( X X. X ) ) ) -> f = ( H ` ( a e. ( X ^m { 0 , 1 } ) |-> ( ( a ` 0 ) f ( a ` 1 ) ) ) ) )
61 6 9 60 rspcedvd 
 |-  ( ( X e. V /\ f e. ( X ^m ( X X. X ) ) ) -> E. g e. ( 2 -aryF X ) f = ( H ` g ) )
62 61 ralrimiva 
 |-  ( X e. V -> A. f e. ( X ^m ( X X. X ) ) E. g e. ( 2 -aryF X ) f = ( H ` g ) )
63 dffo3 
 |-  ( H : ( 2 -aryF X ) -onto-> ( X ^m ( X X. X ) ) <-> ( H : ( 2 -aryF X ) --> ( X ^m ( X X. X ) ) /\ A. f e. ( X ^m ( X X. X ) ) E. g e. ( 2 -aryF X ) f = ( H ` g ) ) )
64 2 62 63 sylanbrc 
 |-  ( X e. V -> H : ( 2 -aryF X ) -onto-> ( X ^m ( X X. X ) ) )