Metamath Proof Explorer

Theorem sgrp0b

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

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

Proof

Step Hyp Ref Expression
1 mgm0b 
 |-  { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } e. Mgm
2 ral0 
 |-  A. x e. (/) A. y e. (/) A. z e. (/) ( ( x ( +g ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } ) y ) ( +g ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } ) z ) = ( x ( +g ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } ) ( y ( +g ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } ) z ) )
3 0ex 
 |-  (/) e. _V
4 eqid 
 |-  { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } = { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. }
5 4 grpbase 
 |-  ( (/) e. _V -> (/) = ( Base ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } ) )
6 3 5 ax-mp 
 |-  (/) = ( Base ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } )
7 eqid 
 |-  ( +g ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } ) = ( +g ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } )
8 6 7 issgrp 
 |-  ( { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } e. Smgrp <-> ( { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } e. Mgm /\ A. x e. (/) A. y e. (/) A. z e. (/) ( ( x ( +g ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } ) y ) ( +g ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } ) z ) = ( x ( +g ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } ) ( y ( +g ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } ) z ) ) ) )
9 1 2 8 mpbir2an 
 |-  { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } e. Smgrp