Theorem grp1

Description: The (smallest) structure representing atrivial group. According to Wikipedia ("Trivial group", 28-Apr-2019, https://en.wikipedia.org/wiki/Trivial_group ) "In mathematics, a trivial group is a group consisting of a single element. All such groups are isomorphic, so one often speaks ofthe trivial group. The single element of the trivial group is the identity element". (Contributed by AV, 28-Apr-2019)

	Ref	Expression
Hypothesis	grp1.m	$$⊢M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{I\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨I,I⟩,I⟩\right\}⟩\right\}$$
Assertion	grp1	$$⊢I\in V\to M\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		grp1.m	$$⊢M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{I\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨I,I⟩,I⟩\right\}⟩\right\}$$
2	1	mnd1	$$⊢I\in V\to M\in \mathrm{Mnd}$$
3		df-ov	$$⊢I\left\{⟨⟨I,I⟩,I⟩\right\}I=\left\{⟨⟨I,I⟩,I⟩\right\}\left(⟨I,I⟩\right)$$
4		opex	$$⊢⟨I,I⟩\in \mathrm{V}$$
5		fvsng	$$⊢\left(⟨I,I⟩\in \mathrm{V}\wedge I\in V\right)\to \left\{⟨⟨I,I⟩,I⟩\right\}\left(⟨I,I⟩\right)=I$$
6	4 5	mpan	$$⊢I\in V\to \left\{⟨⟨I,I⟩,I⟩\right\}\left(⟨I,I⟩\right)=I$$
7	3 6	syl5eq	$$⊢I\in V\to I\left\{⟨⟨I,I⟩,I⟩\right\}I=I$$
8	1	mnd1id	$$⊢I\in V\to 0_M=I$$
9	7 8	eqtr4d	$$⊢I\in V\to I\left\{⟨⟨I,I⟩,I⟩\right\}I=0_M$$
10		oveq2	$$⊢i=I\to e\left\{⟨⟨I,I⟩,I⟩\right\}i=e\left\{⟨⟨I,I⟩,I⟩\right\}I$$
11	10	eqeq1d	$$⊢i=I\to \left(e\left\{⟨⟨I,I⟩,I⟩\right\}i=0_M\leftrightarrow e\left\{⟨⟨I,I⟩,I⟩\right\}I=0_M\right)$$
12	11	rexbidv	$$⊢i=I\to \left(\exists e\in \left\{I\right\}e\left\{⟨⟨I,I⟩,I⟩\right\}i=0_M\leftrightarrow \exists e\in \left\{I\right\}e\left\{⟨⟨I,I⟩,I⟩\right\}I=0_M\right)$$
13	12	ralsng	$$⊢I\in V\to \left(\forall i\in \left\{I\right\}\exists e\in \left\{I\right\}e\left\{⟨⟨I,I⟩,I⟩\right\}i=0_M\leftrightarrow \exists e\in \left\{I\right\}e\left\{⟨⟨I,I⟩,I⟩\right\}I=0_M\right)$$
14		oveq1	$$⊢e=I\to e\left\{⟨⟨I,I⟩,I⟩\right\}I=I\left\{⟨⟨I,I⟩,I⟩\right\}I$$
15	14	eqeq1d	$$⊢e=I\to \left(e\left\{⟨⟨I,I⟩,I⟩\right\}I=0_M\leftrightarrow I\left\{⟨⟨I,I⟩,I⟩\right\}I=0_M\right)$$
16	15	rexsng	$$⊢I\in V\to \left(\exists e\in \left\{I\right\}e\left\{⟨⟨I,I⟩,I⟩\right\}I=0_M\leftrightarrow I\left\{⟨⟨I,I⟩,I⟩\right\}I=0_M\right)$$
17	13 16	bitrd	$$⊢I\in V\to \left(\forall i\in \left\{I\right\}\exists e\in \left\{I\right\}e\left\{⟨⟨I,I⟩,I⟩\right\}i=0_M\leftrightarrow I\left\{⟨⟨I,I⟩,I⟩\right\}I=0_M\right)$$
18	9 17	mpbird	$$⊢I\in V\to \forall i\in \left\{I\right\}\exists e\in \left\{I\right\}e\left\{⟨⟨I,I⟩,I⟩\right\}i=0_M$$
19		snex	$$⊢\left\{I\right\}\in \mathrm{V}$$
20	1	grpbase	$$⊢\left\{I\right\}\in \mathrm{V}\to \left\{I\right\}={\mathrm{Base}}_M$$
21	19 20	ax-mp	$$⊢\left\{I\right\}={\mathrm{Base}}_M$$
22		snex	$$⊢\left\{⟨⟨I,I⟩,I⟩\right\}\in \mathrm{V}$$
23	1	grpplusg	$$⊢\left\{⟨⟨I,I⟩,I⟩\right\}\in \mathrm{V}\to \left\{⟨⟨I,I⟩,I⟩\right\}={+}_M$$
24	22 23	ax-mp	$$⊢\left\{⟨⟨I,I⟩,I⟩\right\}={+}_M$$
25		eqid	$$⊢0_M=0_M$$
26	21 24 25	isgrp	$$⊢M\in \mathrm{Grp}\leftrightarrow \left(M\in \mathrm{Mnd}\wedge \forall i\in \left\{I\right\}\exists e\in \left\{I\right\}e\left\{⟨⟨I,I⟩,I⟩\right\}i=0_M\right)$$
27	2 18 26	sylanbrc	$$⊢I\in V\to M\in \mathrm{Grp}$$