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=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{I\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨I,I⟩,I⟩\right\}⟩\right\}$$
Assertion	mgm1	$$⊢I\in V\to M\in \mathrm{Mgm}$$

Proof

Step	Hyp	Ref	Expression
1		mgm1.m	$$⊢M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{I\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨I,I⟩,I⟩\right\}⟩\right\}$$
2		df-ov	$$⊢I\left\{⟨⟨I,I⟩,I⟩\right\}I=\left\{⟨⟨I,I⟩,I⟩\right\}\left(⟨I,I⟩\right)$$
3		opex	$$⊢⟨I,I⟩\in \mathrm{V}$$
4		fvsng	$$⊢\left(⟨I,I⟩\in \mathrm{V}\wedge I\in V\right)\to \left\{⟨⟨I,I⟩,I⟩\right\}\left(⟨I,I⟩\right)=I$$
5	3 4	mpan	$$⊢I\in V\to \left\{⟨⟨I,I⟩,I⟩\right\}\left(⟨I,I⟩\right)=I$$
6	2 5	syl5eq	$$⊢I\in V\to I\left\{⟨⟨I,I⟩,I⟩\right\}I=I$$
7		snidg	$$⊢I\in V\to I\in \left\{I\right\}$$
8	6 7	eqeltrd	$$⊢I\in V\to I\left\{⟨⟨I,I⟩,I⟩\right\}I\in \left\{I\right\}$$
9		oveq1	$$⊢x=I\to x\left\{⟨⟨I,I⟩,I⟩\right\}y=I\left\{⟨⟨I,I⟩,I⟩\right\}y$$
10	9	eleq1d	$$⊢x=I\to \left(x\left\{⟨⟨I,I⟩,I⟩\right\}y\in \left\{I\right\}\leftrightarrow I\left\{⟨⟨I,I⟩,I⟩\right\}y\in \left\{I\right\}\right)$$
11	10	ralbidv	$$⊢x=I\to \left(\forall y\in \left\{I\right\}x\left\{⟨⟨I,I⟩,I⟩\right\}y\in \left\{I\right\}\leftrightarrow \forall y\in \left\{I\right\}I\left\{⟨⟨I,I⟩,I⟩\right\}y\in \left\{I\right\}\right)$$
12	11	ralsng	$$⊢I\in V\to \left(\forall x\in \left\{I\right\}\forall y\in \left\{I\right\}x\left\{⟨⟨I,I⟩,I⟩\right\}y\in \left\{I\right\}\leftrightarrow \forall y\in \left\{I\right\}I\left\{⟨⟨I,I⟩,I⟩\right\}y\in \left\{I\right\}\right)$$
13		oveq2	$$⊢y=I\to I\left\{⟨⟨I,I⟩,I⟩\right\}y=I\left\{⟨⟨I,I⟩,I⟩\right\}I$$
14	13	eleq1d	$$⊢y=I\to \left(I\left\{⟨⟨I,I⟩,I⟩\right\}y\in \left\{I\right\}\leftrightarrow I\left\{⟨⟨I,I⟩,I⟩\right\}I\in \left\{I\right\}\right)$$
15	14	ralsng	$$⊢I\in V\to \left(\forall y\in \left\{I\right\}I\left\{⟨⟨I,I⟩,I⟩\right\}y\in \left\{I\right\}\leftrightarrow I\left\{⟨⟨I,I⟩,I⟩\right\}I\in \left\{I\right\}\right)$$
16	12 15	bitrd	$$⊢I\in V\to \left(\forall x\in \left\{I\right\}\forall y\in \left\{I\right\}x\left\{⟨⟨I,I⟩,I⟩\right\}y\in \left\{I\right\}\leftrightarrow I\left\{⟨⟨I,I⟩,I⟩\right\}I\in \left\{I\right\}\right)$$
17	8 16	mpbird	$$⊢I\in V\to \forall x\in \left\{I\right\}\forall y\in \left\{I\right\}x\left\{⟨⟨I,I⟩,I⟩\right\}y\in \left\{I\right\}$$
18		snex	$$⊢\left\{I\right\}\in \mathrm{V}$$
19	1	grpbase	$$⊢\left\{I\right\}\in \mathrm{V}\to \left\{I\right\}={\mathrm{Base}}_M$$
20	18 19	ax-mp	$$⊢\left\{I\right\}={\mathrm{Base}}_M$$
21		snex	$$⊢\left\{⟨⟨I,I⟩,I⟩\right\}\in \mathrm{V}$$
22	1	grpplusg	$$⊢\left\{⟨⟨I,I⟩,I⟩\right\}\in \mathrm{V}\to \left\{⟨⟨I,I⟩,I⟩\right\}={+}_M$$
23	21 22	ax-mp	$$⊢\left\{⟨⟨I,I⟩,I⟩\right\}={+}_M$$
24	20 23	ismgmn0	$$⊢I\in \left\{I\right\}\to \left(M\in \mathrm{Mgm}\leftrightarrow \forall x\in \left\{I\right\}\forall y\in \left\{I\right\}x\left\{⟨⟨I,I⟩,I⟩\right\}y\in \left\{I\right\}\right)$$
25	7 24	syl	$$⊢I\in V\to \left(M\in \mathrm{Mgm}\leftrightarrow \forall x\in \left\{I\right\}\forall y\in \left\{I\right\}x\left\{⟨⟨I,I⟩,I⟩\right\}y\in \left\{I\right\}\right)$$
26	17 25	mpbird	$$⊢I\in V\to M\in \mathrm{Mgm}$$