Theorem degenmgmopdm

Description: The domain of the operation of a degenerate magma. (Contributed by AV, 18-Aug-2026)

	Ref	Expression
Hypothesis	degenmgm.m	|- M = { <. ( Base ` ndx ) , { (/) , 1o } >. , <. ( +g ` ndx ) , { <. <. 1o , 1o >. , 1o >. , <. <. 1o , 2o >. , 1o >. , <. <. 1o , (/) >. , 1o >. } >. }
Assertion	degenmgmopdm	|- dom ( +g ` M ) = ( { 1o } X. { (/) , 1o , 2o } )

Proof

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