Metamath Proof Explorer

Theorem degenmgm2opdm

Description: The domain of the operation of a second degenerate magma. (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 degenmgm2opdm 
|- dom ( +g ` M ) = ( { 1o } X. { 1o , 2o } )

Proof

Step Hyp Ref Expression
1 degenmgm2.m 
 |-  M = { <. ( Base ` ndx ) , { (/) , 1o } >. , <. ( +g ` ndx ) , { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } >. }
2 1oex 
 |-  1o e. _V
3 2oex 
 |-  2o e. _V
4 2 2 3 dmtpop 
 |-  dom { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } = { <. 1o , 1o >. , <. 1o , 2o >. , <. 1o , 2o >. }
5 tpex 
 |-  { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } e. _V
6 1 grpplusg 
 |-  ( { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } e. _V -> { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } = ( +g ` M ) )
7 5 6 ax-mp 
 |-  { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. } = ( +g ` M )
8 7 eqcomi 
 |-  ( +g ` M ) = { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. }
9 8 dmeqi 
 |-  dom ( +g ` M ) = dom { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , 2o >. , 2o >. }
10 xpsnprg 
 |-  ( ( 1o e. _V /\ 1o e. _V /\ 2o e. _V ) -> ( { 1o } X. { 1o , 2o } ) = { <. 1o , 1o >. , <. 1o , 2o >. } )
11 2 2 3 10 mp3an 
 |-  ( { 1o } X. { 1o , 2o } ) = { <. 1o , 1o >. , <. 1o , 2o >. }
12 tpidm23 
 |-  { <. 1o , 1o >. , <. 1o , 2o >. , <. 1o , 2o >. } = { <. 1o , 1o >. , <. 1o , 2o >. }
13 11 12 eqtr4i 
 |-  ( { 1o } X. { 1o , 2o } ) = { <. 1o , 1o >. , <. 1o , 2o >. , <. 1o , 2o >. }
14 4 9 13 3eqtr4i 
 |-  dom ( +g ` M ) = ( { 1o } X. { 1o , 2o } )