Metamath Proof Explorer

Theorem degenmgmnfn

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

Ref Expression
Hypotheses degenmgm.m 
|- M = { <. ( Base ` ndx ) , { (/) , 1o } >. , <. ( +g ` ndx ) , { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , (/) >. , 1o >. } >. }
degenmgmbas.b 
|- B = ( Base ` M )
Assertion degenmgmnfn 
|- -. ( +g ` M ) Fn ( B X. B )

Proof

Step Hyp Ref Expression
1 degenmgm.m 
 |-  M = { <. ( Base ` ndx ) , { (/) , 1o } >. , <. ( +g ` ndx ) , { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , (/) >. , 1o >. } >. }
2 degenmgmbas.b 
 |-  B = ( Base ` M )
3 0ex 
 |-  (/) e. _V
4 1oex 
 |-  1o e. _V
5 1n0 
 |-  1o =/= (/)
6 5 necomi 
 |-  (/) =/= 1o
7 prnesn 
 |-  ( ( (/) e. _V /\ 1o e. _V /\ (/) =/= 1o ) -> { (/) , 1o } =/= { 1o } )
8 3 4 6 7 mp3an 
 |-  { (/) , 1o } =/= { 1o }
9 8 nesymi 
 |-  -. { 1o } = { (/) , 1o }
10 9 intnanr 
 |-  -. ( { 1o } = { (/) , 1o } /\ { (/) , 1o , 2o } = { (/) , 1o } )
11 4 snnz 
 |-  { 1o } =/= (/)
12 3 tpnz 
 |-  { (/) , 1o , 2o } =/= (/)
13 xp11 
 |-  ( ( { 1o } =/= (/) /\ { (/) , 1o , 2o } =/= (/) ) -> ( ( { 1o } X. { (/) , 1o , 2o } ) = ( { (/) , 1o } X. { (/) , 1o } ) <-> ( { 1o } = { (/) , 1o } /\ { (/) , 1o , 2o } = { (/) , 1o } ) ) )
14 11 12 13 mp2an 
 |-  ( ( { 1o } X. { (/) , 1o , 2o } ) = ( { (/) , 1o } X. { (/) , 1o } ) <-> ( { 1o } = { (/) , 1o } /\ { (/) , 1o , 2o } = { (/) , 1o } ) )
15 10 14 mtbir 
 |-  -. ( { 1o } X. { (/) , 1o , 2o } ) = ( { (/) , 1o } X. { (/) , 1o } )
16 1 degenmgmopdm 
 |-  dom ( +g ` M ) = ( { 1o } X. { (/) , 1o , 2o } )
17 1 2 degenmgmbas 
 |-  B = { (/) , 1o }
18 17 17 xpeq12i 
 |-  ( B X. B ) = ( { (/) , 1o } X. { (/) , 1o } )
19 16 18 eqeq12i 
 |-  ( dom ( +g ` M ) = ( B X. B ) <-> ( { 1o } X. { (/) , 1o , 2o } ) = ( { (/) , 1o } X. { (/) , 1o } ) )
20 15 19 mtbir 
 |-  -. dom ( +g ` M ) = ( B X. B )
21 20 intnan 
 |-  -. ( Fun ( +g ` M ) /\ dom ( +g ` M ) = ( B X. B ) )
22 df-fn 
 |-  ( ( +g ` M ) Fn ( B X. B ) <-> ( Fun ( +g ` M ) /\ dom ( +g ` M ) = ( B X. B ) ) )
23 21 22 mtbir 
 |-  -. ( +g ` M ) Fn ( B X. B )