Metamath Proof Explorer

Theorem mgm0b

Description: The structure with an empty base set and any group operation is a magma. (Contributed by AV, 28-Aug-2021)

Ref Expression
Assertion mgm0b 
|- { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } e. Mgm

Proof

Step Hyp Ref Expression
1 prex 
 |-  { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } e. _V
2 0ex 
 |-  (/) e. _V
3 eqid 
 |-  { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } = { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. }
4 3 grpbase 
 |-  ( (/) e. _V -> (/) = ( Base ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } ) )
5 4 eqcomd 
 |-  ( (/) e. _V -> ( Base ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } ) = (/) )
6 2 5 ax-mp 
 |-  ( Base ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } ) = (/)
7 mgm0 
 |-  ( ( { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } e. _V /\ ( Base ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } ) = (/) ) -> { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } e. Mgm )
8 1 6 7 mp2an 
 |-  { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } e. Mgm