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 ) ) )