Metamath Proof Explorer

Theorem degenmgm

Description: A degenerate magma: although the operation is not defined for all pairs of elements of the base set ( ( (/) ( +gM ) 1o ) and ( (/) ( +gM ) (/) ) are not defined, and therefore are (/) by definition, which is contained in the base set), and its domain is not (a subset of) the base set ( 2o is in the domain of the operation, but not in the base set) , the structure M is still a magma according to our definition. (Contributed by AV, 18-Aug-2026)

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

Proof

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