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 )