Metamath Proof Explorer


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 = { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. }
Assertion mnd1
|- ( I e. V -> M e. Mnd )

Proof

Step Hyp Ref Expression
1 mnd1.m
 |-  M = { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. }
2 1 sgrp1
 |-  ( I e. V -> M e. Smgrp )
3 df-ov
 |-  ( I { <. <. I , I >. , I >. } I ) = ( { <. <. I , I >. , I >. } ` <. I , I >. )
4 opex
 |-  <. I , I >. e. _V
5 fvsng
 |-  ( ( <. I , I >. e. _V /\ I e. V ) -> ( { <. <. I , I >. , I >. } ` <. I , I >. ) = I )
6 4 5 mpan
 |-  ( I e. V -> ( { <. <. I , I >. , I >. } ` <. I , I >. ) = I )
7 3 6 syl5eq
 |-  ( I e. V -> ( I { <. <. I , I >. , I >. } I ) = I )
8 oveq2
 |-  ( y = I -> ( I { <. <. I , I >. , I >. } y ) = ( I { <. <. I , I >. , I >. } I ) )
9 id
 |-  ( y = I -> y = I )
10 8 9 eqeq12d
 |-  ( y = I -> ( ( I { <. <. I , I >. , I >. } y ) = y <-> ( I { <. <. I , I >. , I >. } I ) = I ) )
11 oveq1
 |-  ( y = I -> ( y { <. <. I , I >. , I >. } I ) = ( I { <. <. I , I >. , I >. } I ) )
12 11 9 eqeq12d
 |-  ( y = I -> ( ( y { <. <. I , I >. , I >. } I ) = y <-> ( I { <. <. I , I >. , I >. } I ) = I ) )
13 10 12 anbi12d
 |-  ( y = I -> ( ( ( I { <. <. I , I >. , I >. } y ) = y /\ ( y { <. <. I , I >. , I >. } I ) = y ) <-> ( ( I { <. <. I , I >. , I >. } I ) = I /\ ( I { <. <. I , I >. , I >. } I ) = I ) ) )
14 13 ralsng
 |-  ( I e. V -> ( A. y e. { I } ( ( I { <. <. I , I >. , I >. } y ) = y /\ ( y { <. <. I , I >. , I >. } I ) = y ) <-> ( ( I { <. <. I , I >. , I >. } I ) = I /\ ( I { <. <. I , I >. , I >. } I ) = I ) ) )
15 7 7 14 mpbir2and
 |-  ( I e. V -> A. y e. { I } ( ( I { <. <. I , I >. , I >. } y ) = y /\ ( y { <. <. I , I >. , I >. } I ) = y ) )
16 oveq1
 |-  ( x = I -> ( x { <. <. I , I >. , I >. } y ) = ( I { <. <. I , I >. , I >. } y ) )
17 16 eqeq1d
 |-  ( x = I -> ( ( x { <. <. I , I >. , I >. } y ) = y <-> ( I { <. <. I , I >. , I >. } y ) = y ) )
18 17 ovanraleqv
 |-  ( x = I -> ( A. y e. { I } ( ( x { <. <. I , I >. , I >. } y ) = y /\ ( y { <. <. I , I >. , I >. } x ) = y ) <-> A. y e. { I } ( ( I { <. <. I , I >. , I >. } y ) = y /\ ( y { <. <. I , I >. , I >. } I ) = y ) ) )
19 18 rexsng
 |-  ( I e. V -> ( E. x e. { I } A. y e. { I } ( ( x { <. <. I , I >. , I >. } y ) = y /\ ( y { <. <. I , I >. , I >. } x ) = y ) <-> A. y e. { I } ( ( I { <. <. I , I >. , I >. } y ) = y /\ ( y { <. <. I , I >. , I >. } I ) = y ) ) )
20 15 19 mpbird
 |-  ( I e. V -> E. x e. { I } A. y e. { I } ( ( x { <. <. I , I >. , I >. } y ) = y /\ ( y { <. <. I , I >. , I >. } x ) = y ) )
21 snex
 |-  { I } e. _V
22 1 grpbase
 |-  ( { I } e. _V -> { I } = ( Base ` M ) )
23 21 22 ax-mp
 |-  { I } = ( Base ` M )
24 snex
 |-  { <. <. I , I >. , I >. } e. _V
25 1 grpplusg
 |-  ( { <. <. I , I >. , I >. } e. _V -> { <. <. I , I >. , I >. } = ( +g ` M ) )
26 24 25 ax-mp
 |-  { <. <. I , I >. , I >. } = ( +g ` M )
27 23 26 ismnddef
 |-  ( 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 ) ) )
28 2 20 27 sylanbrc
 |-  ( I e. V -> M e. Mnd )