This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mgm1

Description: The structure with one element and the only closed internal operation for a singleton is a magma. (Contributed by AV, 10-Feb-2020)

Ref Expression
Hypothesis mgm1.m 
|- M = { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. }
Assertion mgm1 
|- ( I e. V -> M e. Mgm )

Proof

Step Hyp Ref Expression
1 mgm1.m 
 |-  M = { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. }
2 df-ov 
 |-  ( I { <. <. I , I >. , I >. } I ) = ( { <. <. I , I >. , I >. } ` <. I , I >. )
3 opex 
 |-  <. I , I >. e. _V
4 fvsng 
 |-  ( ( <. I , I >. e. _V /\ I e. V ) -> ( { <. <. I , I >. , I >. } ` <. I , I >. ) = I )
5 3 4 mpan 
 |-  ( I e. V -> ( { <. <. I , I >. , I >. } ` <. I , I >. ) = I )
6 2 5 eqtrid 
 |-  ( I e. V -> ( I { <. <. I , I >. , I >. } I ) = I )
7 snidg 
 |-  ( I e. V -> I e. { I } )
8 6 7 eqeltrd 
 |-  ( I e. V -> ( I { <. <. I , I >. , I >. } I ) e. { I } )
9 oveq1 
 |-  ( x = I -> ( x { <. <. I , I >. , I >. } y ) = ( I { <. <. I , I >. , I >. } y ) )
10 9 eleq1d 
 |-  ( x = I -> ( ( x { <. <. I , I >. , I >. } y ) e. { I } <-> ( I { <. <. I , I >. , I >. } y ) e. { I } ) )
11 10 ralbidv 
 |-  ( x = I -> ( A. y e. { I } ( x { <. <. I , I >. , I >. } y ) e. { I } <-> A. y e. { I } ( I { <. <. I , I >. , I >. } y ) e. { I } ) )
12 11 ralsng 
 |-  ( I e. V -> ( A. x e. { I } A. y e. { I } ( x { <. <. I , I >. , I >. } y ) e. { I } <-> A. y e. { I } ( I { <. <. I , I >. , I >. } y ) e. { I } ) )
13 oveq2 
 |-  ( y = I -> ( I { <. <. I , I >. , I >. } y ) = ( I { <. <. I , I >. , I >. } I ) )
14 13 eleq1d 
 |-  ( y = I -> ( ( I { <. <. I , I >. , I >. } y ) e. { I } <-> ( I { <. <. I , I >. , I >. } I ) e. { I } ) )
15 14 ralsng 
 |-  ( I e. V -> ( A. y e. { I } ( I { <. <. I , I >. , I >. } y ) e. { I } <-> ( I { <. <. I , I >. , I >. } I ) e. { I } ) )
16 12 15 bitrd 
 |-  ( I e. V -> ( A. x e. { I } A. y e. { I } ( x { <. <. I , I >. , I >. } y ) e. { I } <-> ( I { <. <. I , I >. , I >. } I ) e. { I } ) )
17 8 16 mpbird 
 |-  ( I e. V -> A. x e. { I } A. y e. { I } ( x { <. <. I , I >. , I >. } y ) e. { I } )
18 snex 
 |-  { I } e. _V
19 1 grpbase 
 |-  ( { I } e. _V -> { I } = ( Base ` M ) )
20 18 19 ax-mp 
 |-  { I } = ( Base ` M )
21 snex 
 |-  { <. <. I , I >. , I >. } e. _V
22 1 grpplusg 
 |-  ( { <. <. I , I >. , I >. } e. _V -> { <. <. I , I >. , I >. } = ( +g ` M ) )
23 21 22 ax-mp 
 |-  { <. <. I , I >. , I >. } = ( +g ` M )
24 20 23 ismgmn0 
 |-  ( I e. { I } -> ( M e. Mgm <-> A. x e. { I } A. y e. { I } ( x { <. <. I , I >. , I >. } y ) e. { I } ) )
25 7 24 syl 
 |-  ( I e. V -> ( M e. Mgm <-> A. x e. { I } A. y e. { I } ( x { <. <. I , I >. , I >. } y ) e. { I } ) )
26 17 25 mpbird 
 |-  ( I e. V -> M e. Mgm )