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 No typesetting found for |- H = ( h e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) ) with typecode |-
Assertion 2arymaptf1 Could not format assertion : No typesetting found for |- ( X e. V -> H : ( 2 -aryF X ) -1-1-> ( X ^m ( X X. X ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 2arymaptf.h Could not format H = ( h e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) ) : No typesetting found for |- H = ( h e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) ) with typecode |-
2 1 2arymaptf Could not format ( X e. V -> H : ( 2 -aryF X ) --> ( X ^m ( X X. X ) ) ) : No typesetting found for |- ( X e. V -> H : ( 2 -aryF X ) --> ( X ^m ( X X. X ) ) ) with typecode |-
3 1 2arymaptfv Could not format ( f e. ( 2 -aryF X ) -> ( H ` f ) = ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) : No typesetting found for |- ( f e. ( 2 -aryF X ) -> ( H ` f ) = ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) with typecode |-
4 3 ad2antrl Could not format ( ( 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 >. } ) ) ) : No typesetting found for |- ( ( 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 >. } ) ) ) with typecode |-
5 1 2arymaptfv Could not format ( g e. ( 2 -aryF X ) -> ( H ` g ) = ( x e. X , y e. X |-> ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) ) : No typesetting found for |- ( g e. ( 2 -aryF X ) -> ( H ` g ) = ( x e. X , y e. X |-> ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) ) with typecode |-
6 5 ad2antll Could not format ( ( 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 >. } ) ) ) : No typesetting found for |- ( ( 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 >. } ) ) ) with typecode |-
7 4 6 eqeq12d Could not format ( ( 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 >. } ) ) ) ) : No typesetting found for |- ( ( 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 >. } ) ) ) ) with typecode |-
8 fvex f 0 x 1 y V
9 8 rgen2w x X y X f 0 x 1 y V
10 mpo2eqb x X y X f 0 x 1 y V x X , y X f 0 x 1 y = x X , y X g 0 x 1 y x X y X f 0 x 1 y = g 0 x 1 y
11 9 10 mp1i Could not format ( ( 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 >. } ) ) ) : No typesetting found for |- ( ( 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 >. } ) ) ) with typecode |-
12 2aryfvalel Could not format ( X e. V -> ( f e. ( 2 -aryF X ) <-> f : ( X ^m { 0 , 1 } ) --> X ) ) : No typesetting found for |- ( X e. V -> ( f e. ( 2 -aryF X ) <-> f : ( X ^m { 0 , 1 } ) --> X ) ) with typecode |-
13 2aryfvalel Could not format ( X e. V -> ( g e. ( 2 -aryF X ) <-> g : ( X ^m { 0 , 1 } ) --> X ) ) : No typesetting found for |- ( X e. V -> ( g e. ( 2 -aryF X ) <-> g : ( X ^m { 0 , 1 } ) --> X ) ) with typecode |-
14 12 13 anbi12d Could not format ( 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 ) ) ) : No typesetting found for |- ( 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 ) ) ) with typecode |-
15 ffn f : X 0 1 X f Fn X 0 1
16 15 adantr f : X 0 1 X g : X 0 1 X f Fn X 0 1
17 16 3ad2ant2 X V f : X 0 1 X g : X 0 1 X x X y X f 0 x 1 y = g 0 x 1 y f Fn X 0 1
18 ffn g : X 0 1 X g Fn X 0 1
19 18 adantl f : X 0 1 X g : X 0 1 X g Fn X 0 1
20 19 3ad2ant2 X V f : X 0 1 X g : X 0 1 X x X y X f 0 x 1 y = g 0 x 1 y g Fn X 0 1
21 elmapi z X 0 1 z : 0 1 X
22 0ne1 0 1
23 c0ex 0 V
24 1ex 1 V
25 23 24 fprb 0 1 z : 0 1 X a X b X z = 0 a 1 b
26 22 25 ax-mp z : 0 1 X a X b X z = 0 a 1 b
27 21 26 sylib z X 0 1 a X b 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 X b X x X y X f 0 x 1 y = g 0 x 1 y f 0 a 1 b = g 0 a 1 b
39 38 expcom x X y X f 0 x 1 y = g 0 x 1 y a X b X f 0 a 1 b = g 0 a 1 b
40 39 3ad2ant3 X V f : X 0 1 X g : X 0 1 X x X y X f 0 x 1 y = g 0 x 1 y a X b X f 0 a 1 b = g 0 a 1 b
41 40 com12 a X b X X V f : X 0 1 X g : X 0 1 X x X y 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 X b X z = 0 a 1 b X V f : X 0 1 X g : X 0 1 X x X y 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 X b 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 X b X z = 0 a 1 b X V f : X 0 1 X g : X 0 1 X x X y X f 0 x 1 y = g 0 x 1 y f z = g z
48 47 ex a X b X z = 0 a 1 b X V f : X 0 1 X g : X 0 1 X x X y X f 0 x 1 y = g 0 x 1 y f z = g z
49 48 rexlimivv a X b X z = 0 a 1 b X V f : X 0 1 X g : X 0 1 X x X y X f 0 x 1 y = g 0 x 1 y f z = g z
50 27 49 syl z X 0 1 X V f : X 0 1 X g : X 0 1 X x X y X f 0 x 1 y = g 0 x 1 y f z = g z
51 50 impcom X V f : X 0 1 X g : X 0 1 X x X y X f 0 x 1 y = g 0 x 1 y z X 0 1 f z = g z
52 17 20 51 eqfnfvd X V f : X 0 1 X g : X 0 1 X x X y X f 0 x 1 y = g 0 x 1 y f = g
53 52 3exp X V f : X 0 1 X g : X 0 1 X x X y X f 0 x 1 y = g 0 x 1 y f = g
54 14 53 sylbid Could not format ( 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 ) ) ) : No typesetting found for |- ( 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 ) ) ) with typecode |-
55 54 imp Could not format ( ( 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 ) ) : No typesetting found for |- ( ( 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 ) ) with typecode |-
56 11 55 sylbid Could not format ( ( 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 ) ) : No typesetting found for |- ( ( 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 ) ) with typecode |-
57 7 56 sylbid Could not format ( ( X e. V /\ ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) ) -> ( ( H ` f ) = ( H ` g ) -> f = g ) ) : No typesetting found for |- ( ( X e. V /\ ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) ) -> ( ( H ` f ) = ( H ` g ) -> f = g ) ) with typecode |-
58 57 ralrimivva Could not format ( X e. V -> A. f e. ( 2 -aryF X ) A. g e. ( 2 -aryF X ) ( ( H ` f ) = ( H ` g ) -> f = g ) ) : No typesetting found for |- ( X e. V -> A. f e. ( 2 -aryF X ) A. g e. ( 2 -aryF X ) ( ( H ` f ) = ( H ` g ) -> f = g ) ) with typecode |-
59 dff13 Could not format ( 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 ) ) ) : No typesetting found for |- ( 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 ) ) ) with typecode |-
60 2 58 59 sylanbrc Could not format ( X e. V -> H : ( 2 -aryF X ) -1-1-> ( X ^m ( X X. X ) ) ) : No typesetting found for |- ( X e. V -> H : ( 2 -aryF X ) -1-1-> ( X ^m ( X X. X ) ) ) with typecode |-