This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem idresefmnd

Description: The structure with the singleton containing only the identity function restricted to a set A as base set and the function composition as group operation, constructed by (structure) restricting the monoid of endofunctions on A to that singleton, is a monoid whose base set is a subset of the base set of the monoid of endofunctions on A . (Contributed by AV, 17-Feb-2024)

Ref Expression
Hypotheses idressubmefmnd.g 
|- G = ( EndoFMnd ` A )
idresefmnd.e 
|- E = ( G |`s { ( _I |` A ) } )
Assertion idresefmnd 
|- ( A e. V -> ( E e. Mnd /\ ( Base ` E ) C_ ( Base ` G ) ) )

Proof

Step Hyp Ref Expression
1 idressubmefmnd.g 
 |-  G = ( EndoFMnd ` A )
2 idresefmnd.e 
 |-  E = ( G |`s { ( _I |` A ) } )
3 1 idressubmefmnd 
 |-  ( A e. V -> { ( _I |` A ) } e. ( SubMnd ` G ) )
4 1 efmndmnd 
 |-  ( A e. V -> G e. Mnd )
5 eqid 
 |-  ( Base ` G ) = ( Base ` G )
6 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
7 eqid 
 |-  ( G |`s { ( _I |` A ) } ) = ( G |`s { ( _I |` A ) } )
8 5 6 7 issubm2 
 |-  ( G e. Mnd -> ( { ( _I |` A ) } e. ( SubMnd ` G ) <-> ( { ( _I |` A ) } C_ ( Base ` G ) /\ ( 0g ` G ) e. { ( _I |` A ) } /\ ( G |`s { ( _I |` A ) } ) e. Mnd ) ) )
9 4 8 syl 
 |-  ( A e. V -> ( { ( _I |` A ) } e. ( SubMnd ` G ) <-> ( { ( _I |` A ) } C_ ( Base ` G ) /\ ( 0g ` G ) e. { ( _I |` A ) } /\ ( G |`s { ( _I |` A ) } ) e. Mnd ) ) )
10 snex 
 |-  { ( _I |` A ) } e. _V
11 2 5 ressbas 
 |-  ( { ( _I |` A ) } e. _V -> ( { ( _I |` A ) } i^i ( Base ` G ) ) = ( Base ` E ) )
12 10 11 mp1i 
 |-  ( A e. V -> ( { ( _I |` A ) } i^i ( Base ` G ) ) = ( Base ` E ) )
13 inss2 
 |-  ( { ( _I |` A ) } i^i ( Base ` G ) ) C_ ( Base ` G )
14 12 13 eqsstrrdi 
 |-  ( A e. V -> ( Base ` E ) C_ ( Base ` G ) )
15 2 eqcomi 
 |-  ( G |`s { ( _I |` A ) } ) = E
16 15 eleq1i 
 |-  ( ( G |`s { ( _I |` A ) } ) e. Mnd <-> E e. Mnd )
17 16 biimpi 
 |-  ( ( G |`s { ( _I |` A ) } ) e. Mnd -> E e. Mnd )
18 17 3ad2ant3 
 |-  ( ( { ( _I |` A ) } C_ ( Base ` G ) /\ ( 0g ` G ) e. { ( _I |` A ) } /\ ( G |`s { ( _I |` A ) } ) e. Mnd ) -> E e. Mnd )
19 14 18 anim12ci 
 |-  ( ( A e. V /\ ( { ( _I |` A ) } C_ ( Base ` G ) /\ ( 0g ` G ) e. { ( _I |` A ) } /\ ( G |`s { ( _I |` A ) } ) e. Mnd ) ) -> ( E e. Mnd /\ ( Base ` E ) C_ ( Base ` G ) ) )
20 19 ex 
 |-  ( A e. V -> ( ( { ( _I |` A ) } C_ ( Base ` G ) /\ ( 0g ` G ) e. { ( _I |` A ) } /\ ( G |`s { ( _I |` A ) } ) e. Mnd ) -> ( E e. Mnd /\ ( Base ` E ) C_ ( Base ` G ) ) ) )
21 9 20 sylbid 
 |-  ( A e. V -> ( { ( _I |` A ) } e. ( SubMnd ` G ) -> ( E e. Mnd /\ ( Base ` E ) C_ ( Base ` G ) ) ) )
22 3 21 mpd 
 |-  ( A e. V -> ( E e. Mnd /\ ( Base ` E ) C_ ( Base ` G ) ) )