Theorem mnd1

Description: The (smallest) structure representing atrivial monoid consists of one element. (Contributed by AV, 28-Apr-2019) (Proof shortened by AV, 11-Feb-2020)

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

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	1	sgrp1	Could not format ( I e. V -> M e. Smgrp ) : No typesetting found for |- ( I e. V -> M e. Smgrp ) with typecode |-
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		oveq2	$$⊢y=I\to I\left\{⟨⟨I,I⟩,I⟩\right\}y=I\left\{⟨⟨I,I⟩,I⟩\right\}I$$
9		id	$$⊢y=I\to y=I$$
10	8 9	eqeq12d	$$⊢y=I\to \left(I\left\{⟨⟨I,I⟩,I⟩\right\}y=y\leftrightarrow I\left\{⟨⟨I,I⟩,I⟩\right\}I=I\right)$$
11		oveq1	$$⊢y=I\to y\left\{⟨⟨I,I⟩,I⟩\right\}I=I\left\{⟨⟨I,I⟩,I⟩\right\}I$$
12	11 9	eqeq12d	$$⊢y=I\to \left(y\left\{⟨⟨I,I⟩,I⟩\right\}I=y\leftrightarrow I\left\{⟨⟨I,I⟩,I⟩\right\}I=I\right)$$
13	10 12	anbi12d	$$⊢y=I\to \left(\left(I\left\{⟨⟨I,I⟩,I⟩\right\}y=y\wedge y\left\{⟨⟨I,I⟩,I⟩\right\}I=y\right)\leftrightarrow \left(I\left\{⟨⟨I,I⟩,I⟩\right\}I=I\wedge I\left\{⟨⟨I,I⟩,I⟩\right\}I=I\right)\right)$$
14	13	ralsng	$$⊢I\in V\to \left(\forall y\in \left\{I\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}y=y\wedge y\left\{⟨⟨I,I⟩,I⟩\right\}I=y\right)\leftrightarrow \left(I\left\{⟨⟨I,I⟩,I⟩\right\}I=I\wedge I\left\{⟨⟨I,I⟩,I⟩\right\}I=I\right)\right)$$
15	7 7 14	mpbir2and	$$⊢I\in V\to \forall y\in \left\{I\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}y=y\wedge y\left\{⟨⟨I,I⟩,I⟩\right\}I=y\right)$$
16		oveq1	$$⊢x=I\to x\left\{⟨⟨I,I⟩,I⟩\right\}y=I\left\{⟨⟨I,I⟩,I⟩\right\}y$$
17	16	eqeq1d	$$⊢x=I\to \left(x\left\{⟨⟨I,I⟩,I⟩\right\}y=y\leftrightarrow I\left\{⟨⟨I,I⟩,I⟩\right\}y=y\right)$$
18	17	ovanraleqv	$$⊢x=I\to \left(\forall y\in \left\{I\right\}\left(x\left\{⟨⟨I,I⟩,I⟩\right\}y=y\wedge y\left\{⟨⟨I,I⟩,I⟩\right\}x=y\right)\leftrightarrow \forall y\in \left\{I\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}y=y\wedge y\left\{⟨⟨I,I⟩,I⟩\right\}I=y\right)\right)$$
19	18	rexsng	$$⊢I\in V\to \left(\exists x\in \left\{I\right\}\forall y\in \left\{I\right\}\left(x\left\{⟨⟨I,I⟩,I⟩\right\}y=y\wedge y\left\{⟨⟨I,I⟩,I⟩\right\}x=y\right)\leftrightarrow \forall y\in \left\{I\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}y=y\wedge y\left\{⟨⟨I,I⟩,I⟩\right\}I=y\right)\right)$$
20	15 19	mpbird	$$⊢I\in V\to \exists x\in \left\{I\right\}\forall y\in \left\{I\right\}\left(x\left\{⟨⟨I,I⟩,I⟩\right\}y=y\wedge y\left\{⟨⟨I,I⟩,I⟩\right\}x=y\right)$$
21		snex	$$⊢\left\{I\right\}\in \mathrm{V}$$
22	1	grpbase	$$⊢\left\{I\right\}\in \mathrm{V}\to \left\{I\right\}={\mathrm{Base}}_M$$
23	21 22	ax-mp	$$⊢\left\{I\right\}={\mathrm{Base}}_M$$
24		snex	$$⊢\left\{⟨⟨I,I⟩,I⟩\right\}\in \mathrm{V}$$
25	1	grpplusg	$$⊢\left\{⟨⟨I,I⟩,I⟩\right\}\in \mathrm{V}\to \left\{⟨⟨I,I⟩,I⟩\right\}={+}_M$$
26	24 25	ax-mp	$$⊢\left\{⟨⟨I,I⟩,I⟩\right\}={+}_M$$
27	23 26	ismnddef	Could not format ( M e. Mnd <-> ( M e. Smgrp /\ E. x e. { I } A. y e. { I } ( ( x { <. <. I , I >. , I >. } y ) = y /\ ( y { <. <. I , I >. , I >. } x ) = y ) ) ) : No typesetting found for |- ( M e. Mnd <-> ( M e. Smgrp /\ E. x e. { I } A. y e. { I } ( ( x { <. <. I , I >. , I >. } y ) = y /\ ( y { <. <. I , I >. , I >. } x ) = y ) ) ) with typecode |-
28	2 20 27	sylanbrc	$$⊢I\in V\to M\in \mathrm{Mnd}$$