Metamath Proof Explorer

Theorem degenmgm2nfun

Description: The operation of a second degenerate magma is not a function. (Contributed by AV, 21-Aug-2026)

Ref Expression
Hypothesis degenmgm2.m 
|- M = { <. ( Base ` ndx ) , { (/) , 1o } >. , <. ( +g ` ndx ) , { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } >. }
Assertion degenmgm2nfun 
|- -. Fun ( +g ` M )

Proof

Step Hyp Ref Expression
1 degenmgm2.m 
 |-  M = { <. ( Base ` ndx ) , { (/) , 1o } >. , <. ( +g ` ndx ) , { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } >. }
2 2oex 
 |-  2o e. _V
3 opeq2 
 |-  ( z = 2o -> <. <. 1o , 2o >. , z >. = <. <. 1o , 2o >. , 2o >. )
4 3 eleq1d 
 |-  ( z = 2o -> ( <. <. 1o , 2o >. , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } <-> <. <. 1o , 2o >. , 2o >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) )
5 4 anbi2d 
 |-  ( z = 2o -> ( ( <. <. 1o , 2o >. , 1o >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. <. 1o , 2o >. , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) <-> ( <. <. 1o , 2o >. , 1o >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. <. 1o , 2o >. , 2o >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) ) )
6 eqeq2 
 |-  ( z = 2o -> ( 1o = z <-> 1o = 2o ) )
7 6 necon3bbid 
 |-  ( z = 2o -> ( -. 1o = z <-> 1o =/= 2o ) )
8 5 7 anbi12d 
 |-  ( z = 2o -> ( ( ( <. <. 1o , 2o >. , 1o >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. <. 1o , 2o >. , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) /\ -. 1o = z ) <-> ( ( <. <. 1o , 2o >. , 1o >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. <. 1o , 2o >. , 2o >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) /\ 1o =/= 2o ) ) )
9 opex 
 |-  <. <. 1o , 2o >. , 1o >. e. _V
10 9 tpid2 
 |-  <. <. 1o , 2o >. , 1o >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. }
11 opex 
 |-  <. <. 1o , 2o >. , 2o >. e. _V
12 11 tpid3 
 |-  <. <. 1o , 2o >. , 2o >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. }
13 10 12 pm3.2i 
 |-  ( <. <. 1o , 2o >. , 1o >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. <. 1o , 2o >. , 2o >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } )
14 1one2o 
 |-  1o =/= 2o
15 13 14 pm3.2i 
 |-  ( ( <. <. 1o , 2o >. , 1o >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. <. 1o , 2o >. , 2o >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) /\ 1o =/= 2o )
16 2 8 15 ceqsexv2d 
 |-  E. z ( ( <. <. 1o , 2o >. , 1o >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. <. 1o , 2o >. , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) /\ -. 1o = z )
17 opex 
 |-  <. 1o , 2o >. e. _V
18 1oex 
 |-  1o e. _V
19 opeq12 
 |-  ( ( x = <. 1o , 2o >. /\ y = 1o ) -> <. x , y >. = <. <. 1o , 2o >. , 1o >. )
20 19 eleq1d 
 |-  ( ( x = <. 1o , 2o >. /\ y = 1o ) -> ( <. x , y >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } <-> <. <. 1o , 2o >. , 1o >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) )
21 opeq1 
 |-  ( x = <. 1o , 2o >. -> <. x , z >. = <. <. 1o , 2o >. , z >. )
22 21 adantr 
 |-  ( ( x = <. 1o , 2o >. /\ y = 1o ) -> <. x , z >. = <. <. 1o , 2o >. , z >. )
23 22 eleq1d 
 |-  ( ( x = <. 1o , 2o >. /\ y = 1o ) -> ( <. x , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } <-> <. <. 1o , 2o >. , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) )
24 20 23 anbi12d 
 |-  ( ( x = <. 1o , 2o >. /\ y = 1o ) -> ( ( <. x , y >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. x , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) <-> ( <. <. 1o , 2o >. , 1o >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. <. 1o , 2o >. , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) ) )
25 eqeq1 
 |-  ( y = 1o -> ( y = z <-> 1o = z ) )
26 25 adantl 
 |-  ( ( x = <. 1o , 2o >. /\ y = 1o ) -> ( y = z <-> 1o = z ) )
27 24 26 imbi12d 
 |-  ( ( x = <. 1o , 2o >. /\ y = 1o ) -> ( ( ( <. x , y >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. x , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) -> y = z ) <-> ( ( <. <. 1o , 2o >. , 1o >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. <. 1o , 2o >. , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) -> 1o = z ) ) )
28 27 notbid 
 |-  ( ( x = <. 1o , 2o >. /\ y = 1o ) -> ( -. ( ( <. x , y >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. x , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) -> y = z ) <-> -. ( ( <. <. 1o , 2o >. , 1o >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. <. 1o , 2o >. , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) -> 1o = z ) ) )
29 pm4.61 
 |-  ( -. ( ( <. <. 1o , 2o >. , 1o >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. <. 1o , 2o >. , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) -> 1o = z ) <-> ( ( <. <. 1o , 2o >. , 1o >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. <. 1o , 2o >. , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) /\ -. 1o = z ) )
30 28 29 bitrdi 
 |-  ( ( x = <. 1o , 2o >. /\ y = 1o ) -> ( -. ( ( <. x , y >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. x , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) -> y = z ) <-> ( ( <. <. 1o , 2o >. , 1o >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. <. 1o , 2o >. , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) /\ -. 1o = z ) ) )
31 30 exbidv 
 |-  ( ( x = <. 1o , 2o >. /\ y = 1o ) -> ( E. z -. ( ( <. x , y >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. x , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) -> y = z ) <-> E. z ( ( <. <. 1o , 2o >. , 1o >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. <. 1o , 2o >. , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) /\ -. 1o = z ) ) )
32 17 18 31 spc2ev 
 |-  ( E. z ( ( <. <. 1o , 2o >. , 1o >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. <. 1o , 2o >. , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) /\ -. 1o = z ) -> E. x E. y E. z -. ( ( <. x , y >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. x , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) -> y = z ) )
33 16 32 ax-mp 
 |-  E. x E. y E. z -. ( ( <. x , y >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. x , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) -> y = z )
34 exnal 
 |-  ( E. z -. ( ( <. x , y >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. x , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) -> y = z ) <-> -. A. z ( ( <. x , y >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. x , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) -> y = z ) )
35 34 bicomi 
 |-  ( -. A. z ( ( <. x , y >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. x , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) -> y = z ) <-> E. z -. ( ( <. x , y >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. x , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) -> y = z ) )
36 35 2exbii 
 |-  ( E. x E. y -. A. z ( ( <. x , y >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. x , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) -> y = z ) <-> E. x E. y E. z -. ( ( <. x , y >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. x , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) -> y = z ) )
37 33 36 mpbir 
 |-  E. x E. y -. A. z ( ( <. x , y >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. x , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) -> y = z )
38 2nalexn 
 |-  ( -. A. x A. y A. z ( ( <. x , y >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. x , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) -> y = z ) <-> E. x E. y -. A. z ( ( <. x , y >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. x , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) -> y = z ) )
39 37 38 mpbir 
 |-  -. A. x A. y A. z ( ( <. x , y >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. x , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) -> y = z )
40 39 intnan 
 |-  -. ( Rel { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ A. x A. y A. z ( ( <. x , y >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. x , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) -> y = z ) )
41 tpex 
 |-  { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } e. _V
42 1 grpplusg 
 |-  ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } e. _V -> { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } = ( +g ` M ) )
43 41 42 ax-mp 
 |-  { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } = ( +g ` M )
44 43 eqcomi 
 |-  ( +g ` M ) = { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. }
45 44 funeqi 
 |-  ( Fun ( +g ` M ) <-> Fun { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } )
46 dffun4 
 |-  ( Fun { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } <-> ( Rel { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ A. x A. y A. z ( ( <. x , y >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. x , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) -> y = z ) ) )
47 45 46 bitri 
 |-  ( Fun ( +g ` M ) <-> ( Rel { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ A. x A. y A. z ( ( <. x , y >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } /\ <. x , z >. e. { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ) -> y = z ) ) )
48 40 47 mtbir 
 |-  -. Fun ( +g ` M )