Metamath Proof Explorer

Theorem degenmgm2

Description: A degenerate magma: although the operation is not defined for all pairs of elements of the base set, and its domain is not (a subset of) the base set, and the operation is not a function (see degenmgm2nfun ), the structure M is still a magma according to our definition. (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 degenmgm2 
|- M e. Mgm

Proof

Step Hyp Ref Expression
1 degenmgm2.m 
 |-  M = { <. ( Base ` ndx ) , { (/) , 1o } >. , <. ( +g ` ndx ) , { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } >. }
2 0ex 
 |-  (/) e. _V
3 2 prid1 
 |-  (/) e. { (/) , 1o }
4 3 3 pm3.2i 
 |-  ( (/) e. { (/) , 1o } /\ (/) e. { (/) , 1o } )
5 1oelpr 
 |-  1o e. { (/) , 1o }
6 3 5 pm3.2i 
 |-  ( (/) e. { (/) , 1o } /\ 1o e. { (/) , 1o } )
7 4 6 pm3.2i 
 |-  ( ( (/) e. { (/) , 1o } /\ (/) e. { (/) , 1o } ) /\ ( (/) e. { (/) , 1o } /\ 1o e. { (/) , 1o } ) )
8 1oex 
 |-  1o e. _V
9 oveq1 
 |-  ( x = (/) -> ( x { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } y ) = ( (/) { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } y ) )
10 df-ov 
 |-  ( (/) { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } y ) = ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. (/) , y >. )
11 9 10 eqtrdi 
 |-  ( x = (/) -> ( x { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } y ) = ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. (/) , y >. ) )
12 11 eleq1d 
 |-  ( x = (/) -> ( ( x { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } y ) e. { (/) , 1o } <-> ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. (/) , y >. ) e. { (/) , 1o } ) )
13 12 ralbidv 
 |-  ( x = (/) -> ( A. y e. { (/) , 1o } ( x { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } y ) e. { (/) , 1o } <-> A. y e. { (/) , 1o } ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. (/) , y >. ) e. { (/) , 1o } ) )
14 oveq1 
 |-  ( x = 1o -> ( x { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } y ) = ( 1o { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } y ) )
15 df-ov 
 |-  ( 1o { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } y ) = ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. 1o , y >. )
16 14 15 eqtrdi 
 |-  ( x = 1o -> ( x { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } y ) = ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. 1o , y >. ) )
17 16 eleq1d 
 |-  ( x = 1o -> ( ( x { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } y ) e. { (/) , 1o } <-> ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. 1o , y >. ) e. { (/) , 1o } ) )
18 17 ralbidv 
 |-  ( x = 1o -> ( A. y e. { (/) , 1o } ( x { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } y ) e. { (/) , 1o } <-> A. y e. { (/) , 1o } ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. 1o , y >. ) e. { (/) , 1o } ) )
19 2 8 13 18 ralpr 
 |-  ( A. x e. { (/) , 1o } A. y e. { (/) , 1o } ( x { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } y ) e. { (/) , 1o } <-> ( A. y e. { (/) , 1o } ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. (/) , y >. ) e. { (/) , 1o } /\ A. y e. { (/) , 1o } ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. 1o , y >. ) e. { (/) , 1o } ) )
20 opeq2 
 |-  ( y = (/) -> <. (/) , y >. = <. (/) , (/) >. )
21 20 fveq2d 
 |-  ( y = (/) -> ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. (/) , y >. ) = ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. (/) , (/) >. ) )
22 1n0 
 |-  1o =/= (/)
23 22 necomi 
 |-  (/) =/= 1o
24 23 orci 
 |-  ( (/) =/= 1o \/ (/) =/= 1o )
25 2 2 opthne 
 |-  ( <. (/) , (/) >. =/= <. 1o , 1o >. <-> ( (/) =/= 1o \/ (/) =/= 1o ) )
26 24 25 mpbir 
 |-  <. (/) , (/) >. =/= <. 1o , 1o >.
27 23 orci 
 |-  ( (/) =/= 1o \/ (/) =/= 2o )
28 2 2 opthne 
 |-  ( <. (/) , (/) >. =/= <. 1o , 2o >. <-> ( (/) =/= 1o \/ (/) =/= 2o ) )
29 27 28 mpbir 
 |-  <. (/) , (/) >. =/= <. 1o , 2o >.
30 2oex 
 |-  2o e. _V
31 opex 
 |-  <. (/) , (/) >. e. _V
32 8 8 30 31 fvtp0 
 |-  ( ( <. (/) , (/) >. =/= <. 1o , 1o >. /\ <. (/) , (/) >. =/= <. 1o , 2o >. /\ <. (/) , (/) >. =/= <. 1o , 2o >. ) -> ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. (/) , (/) >. ) = (/) )
33 26 29 29 32 mp3an 
 |-  ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. (/) , (/) >. ) = (/)
34 21 33 eqtrdi 
 |-  ( y = (/) -> ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. (/) , y >. ) = (/) )
35 34 eleq1d 
 |-  ( y = (/) -> ( ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. (/) , y >. ) e. { (/) , 1o } <-> (/) e. { (/) , 1o } ) )
36 opeq2 
 |-  ( y = 1o -> <. (/) , y >. = <. (/) , 1o >. )
37 36 fveq2d 
 |-  ( y = 1o -> ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. (/) , y >. ) = ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. (/) , 1o >. ) )
38 23 orci 
 |-  ( (/) =/= 1o \/ 1o =/= 1o )
39 2 8 opthne 
 |-  ( <. (/) , 1o >. =/= <. 1o , 1o >. <-> ( (/) =/= 1o \/ 1o =/= 1o ) )
40 38 39 mpbir 
 |-  <. (/) , 1o >. =/= <. 1o , 1o >.
41 23 orci 
 |-  ( (/) =/= 1o \/ 1o =/= 2o )
42 2 8 opthne 
 |-  ( <. (/) , 1o >. =/= <. 1o , 2o >. <-> ( (/) =/= 1o \/ 1o =/= 2o ) )
43 41 42 mpbir 
 |-  <. (/) , 1o >. =/= <. 1o , 2o >.
44 1one2o 
 |-  1o =/= 2o
45 44 olci 
 |-  ( (/) =/= 1o \/ 1o =/= 2o )
46 45 42 mpbir 
 |-  <. (/) , 1o >. =/= <. 1o , 2o >.
47 opex 
 |-  <. (/) , 1o >. e. _V
48 8 8 30 47 fvtp0 
 |-  ( ( <. (/) , 1o >. =/= <. 1o , 1o >. /\ <. (/) , 1o >. =/= <. 1o , 2o >. /\ <. (/) , 1o >. =/= <. 1o , 2o >. ) -> ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. (/) , 1o >. ) = (/) )
49 40 43 46 48 mp3an 
 |-  ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. (/) , 1o >. ) = (/)
50 37 49 eqtrdi 
 |-  ( y = 1o -> ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. (/) , y >. ) = (/) )
51 50 eleq1d 
 |-  ( y = 1o -> ( ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. (/) , y >. ) e. { (/) , 1o } <-> (/) e. { (/) , 1o } ) )
52 2 8 35 51 ralpr 
 |-  ( A. y e. { (/) , 1o } ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. (/) , y >. ) e. { (/) , 1o } <-> ( (/) e. { (/) , 1o } /\ (/) e. { (/) , 1o } ) )
53 opeq2 
 |-  ( y = (/) -> <. 1o , y >. = <. 1o , (/) >. )
54 53 fveq2d 
 |-  ( y = (/) -> ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. 1o , y >. ) = ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. 1o , (/) >. ) )
55 23 olci 
 |-  ( 1o =/= 1o \/ (/) =/= 1o )
56 8 2 opthne 
 |-  ( <. 1o , (/) >. =/= <. 1o , 1o >. <-> ( 1o =/= 1o \/ (/) =/= 1o ) )
57 55 56 mpbir 
 |-  <. 1o , (/) >. =/= <. 1o , 1o >.
58 2on0 
 |-  2o =/= (/)
59 58 olci 
 |-  ( 1o =/= 1o \/ 2o =/= (/) )
60 8 30 opthne 
 |-  ( <. 1o , 2o >. =/= <. 1o , (/) >. <-> ( 1o =/= 1o \/ 2o =/= (/) ) )
61 59 60 mpbir 
 |-  <. 1o , 2o >. =/= <. 1o , (/) >.
62 61 necomi 
 |-  <. 1o , (/) >. =/= <. 1o , 2o >.
63 opex 
 |-  <. 1o , (/) >. e. _V
64 8 8 30 63 fvtp0 
 |-  ( ( <. 1o , (/) >. =/= <. 1o , 1o >. /\ <. 1o , (/) >. =/= <. 1o , 2o >. /\ <. 1o , (/) >. =/= <. 1o , 2o >. ) -> ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. 1o , (/) >. ) = (/) )
65 57 62 62 64 mp3an 
 |-  ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. 1o , (/) >. ) = (/)
66 54 65 eqtrdi 
 |-  ( y = (/) -> ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. 1o , y >. ) = (/) )
67 66 eleq1d 
 |-  ( y = (/) -> ( ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. 1o , y >. ) e. { (/) , 1o } <-> (/) e. { (/) , 1o } ) )
68 opeq2 
 |-  ( y = 1o -> <. 1o , y >. = <. 1o , 1o >. )
69 68 fveq2d 
 |-  ( y = 1o -> ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. 1o , y >. ) = ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. 1o , 1o >. ) )
70 44 olci 
 |-  ( 1o =/= 1o \/ 1o =/= 2o )
71 8 8 opthne 
 |-  ( <. 1o , 1o >. =/= <. 1o , 2o >. <-> ( 1o =/= 1o \/ 1o =/= 2o ) )
72 70 71 mpbir 
 |-  <. 1o , 1o >. =/= <. 1o , 2o >.
73 opex 
 |-  <. 1o , 1o >. e. _V
74 73 8 fvtp1 
 |-  ( ( <. 1o , 1o >. =/= <. 1o , 2o >. /\ <. 1o , 1o >. =/= <. 1o , 2o >. ) -> ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. 1o , 1o >. ) = 1o )
75 72 72 74 mp2an 
 |-  ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. 1o , 1o >. ) = 1o
76 69 75 eqtrdi 
 |-  ( y = 1o -> ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. 1o , y >. ) = 1o )
77 76 eleq1d 
 |-  ( y = 1o -> ( ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. 1o , y >. ) e. { (/) , 1o } <-> 1o e. { (/) , 1o } ) )
78 2 8 67 77 ralpr 
 |-  ( A. y e. { (/) , 1o } ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. 1o , y >. ) e. { (/) , 1o } <-> ( (/) e. { (/) , 1o } /\ 1o e. { (/) , 1o } ) )
79 52 78 anbi12i 
 |-  ( ( A. y e. { (/) , 1o } ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. (/) , y >. ) e. { (/) , 1o } /\ A. y e. { (/) , 1o } ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } ` <. 1o , y >. ) e. { (/) , 1o } ) <-> ( ( (/) e. { (/) , 1o } /\ (/) e. { (/) , 1o } ) /\ ( (/) e. { (/) , 1o } /\ 1o e. { (/) , 1o } ) ) )
80 19 79 bitri 
 |-  ( A. x e. { (/) , 1o } A. y e. { (/) , 1o } ( x { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } y ) e. { (/) , 1o } <-> ( ( (/) e. { (/) , 1o } /\ (/) e. { (/) , 1o } ) /\ ( (/) e. { (/) , 1o } /\ 1o e. { (/) , 1o } ) ) )
81 7 80 mpbir 
 |-  A. x e. { (/) , 1o } A. y e. { (/) , 1o } ( x { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } y ) e. { (/) , 1o }
82 prex 
 |-  { (/) , 1o } e. _V
83 1 grpbase 
 |-  ( { (/) , 1o } e. _V -> { (/) , 1o } = ( Base ` M ) )
84 82 83 ax-mp 
 |-  { (/) , 1o } = ( Base ` M )
85 tpex 
 |-  { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } e. _V
86 1 grpplusg 
 |-  ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } e. _V -> { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } = ( +g ` M ) )
87 85 86 ax-mp 
 |-  { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } = ( +g ` M )
88 84 87 ismgmn0 
 |-  ( (/) e. { (/) , 1o } -> ( M e. Mgm <-> A. x e. { (/) , 1o } A. y e. { (/) , 1o } ( x { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } y ) e. { (/) , 1o } ) )
89 81 88 mpbiri 
 |-  ( (/) e. { (/) , 1o } -> M e. Mgm )
90 3 89 ax-mp 
 |-  M e. Mgm