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 )