Theorem mnd1id

Description: The singleton element of atrivial monoid is its identity element. (Contributed by FL, 21-Jun-2010) (Revised by AV, 23-Jan-2020)

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

Proof

Step	Hyp	Ref	Expression
1		mnd1.m	$$⊢M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{I\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨I,I⟩,I⟩\right\}⟩\right\}$$
2		snex	$$⊢\left\{I\right\}\in \mathrm{V}$$
3	1	grpbase	$$⊢\left\{I\right\}\in \mathrm{V}\to \left\{I\right\}={\mathrm{Base}}_M$$
4	2 3	ax-mp	$$⊢\left\{I\right\}={\mathrm{Base}}_M$$
5		eqid	$$⊢0_M=0_M$$
6		snex	$$⊢\left\{⟨⟨I,I⟩,I⟩\right\}\in \mathrm{V}$$
7	1	grpplusg	$$⊢\left\{⟨⟨I,I⟩,I⟩\right\}\in \mathrm{V}\to \left\{⟨⟨I,I⟩,I⟩\right\}={+}_M$$
8	6 7	ax-mp	$$⊢\left\{⟨⟨I,I⟩,I⟩\right\}={+}_M$$
9		snidg	$$⊢I\in V\to I\in \left\{I\right\}$$
10		velsn	$$⊢a\in \left\{I\right\}\leftrightarrow a=I$$
11		df-ov	$$⊢I\left\{⟨⟨I,I⟩,I⟩\right\}I=\left\{⟨⟨I,I⟩,I⟩\right\}\left(⟨I,I⟩\right)$$
12		opex	$$⊢⟨I,I⟩\in \mathrm{V}$$
13		fvsng	$$⊢\left(⟨I,I⟩\in \mathrm{V}\wedge I\in V\right)\to \left\{⟨⟨I,I⟩,I⟩\right\}\left(⟨I,I⟩\right)=I$$
14	12 13	mpan	$$⊢I\in V\to \left\{⟨⟨I,I⟩,I⟩\right\}\left(⟨I,I⟩\right)=I$$
15	11 14	eqtrid	$$⊢I\in V\to I\left\{⟨⟨I,I⟩,I⟩\right\}I=I$$
16		oveq2	$$⊢a=I\to I\left\{⟨⟨I,I⟩,I⟩\right\}a=I\left\{⟨⟨I,I⟩,I⟩\right\}I$$
17		id	$$⊢a=I\to a=I$$
18	16 17	eqeq12d	$$⊢a=I\to \left(I\left\{⟨⟨I,I⟩,I⟩\right\}a=a\leftrightarrow I\left\{⟨⟨I,I⟩,I⟩\right\}I=I\right)$$
19	15 18	syl5ibrcom	$$⊢I\in V\to \left(a=I\to I\left\{⟨⟨I,I⟩,I⟩\right\}a=a\right)$$
20	10 19	biimtrid	$$⊢I\in V\to \left(a\in \left\{I\right\}\to I\left\{⟨⟨I,I⟩,I⟩\right\}a=a\right)$$
21	20	imp	$$⊢\left(I\in V\wedge a\in \left\{I\right\}\right)\to I\left\{⟨⟨I,I⟩,I⟩\right\}a=a$$
22		oveq1	$$⊢a=I\to a\left\{⟨⟨I,I⟩,I⟩\right\}I=I\left\{⟨⟨I,I⟩,I⟩\right\}I$$
23	22 17	eqeq12d	$$⊢a=I\to \left(a\left\{⟨⟨I,I⟩,I⟩\right\}I=a\leftrightarrow I\left\{⟨⟨I,I⟩,I⟩\right\}I=I\right)$$
24	15 23	syl5ibrcom	$$⊢I\in V\to \left(a=I\to a\left\{⟨⟨I,I⟩,I⟩\right\}I=a\right)$$
25	10 24	biimtrid	$$⊢I\in V\to \left(a\in \left\{I\right\}\to a\left\{⟨⟨I,I⟩,I⟩\right\}I=a\right)$$
26	25	imp	$$⊢\left(I\in V\wedge a\in \left\{I\right\}\right)\to a\left\{⟨⟨I,I⟩,I⟩\right\}I=a$$
27	4 5 8 9 21 26	ismgmid2	$$⊢I\in V\to I=0_M$$
28	27	eqcomd	$$⊢I\in V\to 0_M=I$$