Metamath Proof Explorer


Theorem sursubmefmnd

Description: The set of surjective endofunctions on a set A is a submonoid of the monoid of endofunctions on A . (Contributed by AV, 25-Feb-2024)

Ref Expression
Hypothesis sursubmefmnd.m
|- M = ( EndoFMnd ` A )
Assertion sursubmefmnd
|- ( A e. V -> { h | h : A -onto-> A } e. ( SubMnd ` M ) )

Proof

Step Hyp Ref Expression
1 sursubmefmnd.m
 |-  M = ( EndoFMnd ` A )
2 vex
 |-  x e. _V
3 foeq1
 |-  ( h = x -> ( h : A -onto-> A <-> x : A -onto-> A ) )
4 2 3 elab
 |-  ( x e. { h | h : A -onto-> A } <-> x : A -onto-> A )
5 fof
 |-  ( x : A -onto-> A -> x : A --> A )
6 eqid
 |-  ( Base ` M ) = ( Base ` M )
7 1 6 elefmndbas
 |-  ( A e. V -> ( x e. ( Base ` M ) <-> x : A --> A ) )
8 5 7 syl5ibr
 |-  ( A e. V -> ( x : A -onto-> A -> x e. ( Base ` M ) ) )
9 4 8 syl5bi
 |-  ( A e. V -> ( x e. { h | h : A -onto-> A } -> x e. ( Base ` M ) ) )
10 9 ssrdv
 |-  ( A e. V -> { h | h : A -onto-> A } C_ ( Base ` M ) )
11 1 efmndid
 |-  ( A e. V -> ( _I |` A ) = ( 0g ` M ) )
12 resiexg
 |-  ( A e. V -> ( _I |` A ) e. _V )
13 f1oi
 |-  ( _I |` A ) : A -1-1-onto-> A
14 f1ofo
 |-  ( ( _I |` A ) : A -1-1-onto-> A -> ( _I |` A ) : A -onto-> A )
15 13 14 mp1i
 |-  ( A e. V -> ( _I |` A ) : A -onto-> A )
16 foeq1
 |-  ( h = ( _I |` A ) -> ( h : A -onto-> A <-> ( _I |` A ) : A -onto-> A ) )
17 12 15 16 elabd
 |-  ( A e. V -> ( _I |` A ) e. { h | h : A -onto-> A } )
18 11 17 eqeltrrd
 |-  ( A e. V -> ( 0g ` M ) e. { h | h : A -onto-> A } )
19 vex
 |-  y e. _V
20 foeq1
 |-  ( h = y -> ( h : A -onto-> A <-> y : A -onto-> A ) )
21 19 20 elab
 |-  ( y e. { h | h : A -onto-> A } <-> y : A -onto-> A )
22 4 21 anbi12i
 |-  ( ( x e. { h | h : A -onto-> A } /\ y e. { h | h : A -onto-> A } ) <-> ( x : A -onto-> A /\ y : A -onto-> A ) )
23 foco
 |-  ( ( x : A -onto-> A /\ y : A -onto-> A ) -> ( x o. y ) : A -onto-> A )
24 23 adantl
 |-  ( ( A e. V /\ ( x : A -onto-> A /\ y : A -onto-> A ) ) -> ( x o. y ) : A -onto-> A )
25 fof
 |-  ( y : A -onto-> A -> y : A --> A )
26 5 25 anim12i
 |-  ( ( x : A -onto-> A /\ y : A -onto-> A ) -> ( x : A --> A /\ y : A --> A ) )
27 1 6 elefmndbas
 |-  ( A e. V -> ( y e. ( Base ` M ) <-> y : A --> A ) )
28 7 27 anbi12d
 |-  ( A e. V -> ( ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) <-> ( x : A --> A /\ y : A --> A ) ) )
29 26 28 syl5ibr
 |-  ( A e. V -> ( ( x : A -onto-> A /\ y : A -onto-> A ) -> ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) )
30 29 imp
 |-  ( ( A e. V /\ ( x : A -onto-> A /\ y : A -onto-> A ) ) -> ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) )
31 eqid
 |-  ( +g ` M ) = ( +g ` M )
32 1 6 31 efmndov
 |-  ( ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) -> ( x ( +g ` M ) y ) = ( x o. y ) )
33 30 32 syl
 |-  ( ( A e. V /\ ( x : A -onto-> A /\ y : A -onto-> A ) ) -> ( x ( +g ` M ) y ) = ( x o. y ) )
34 33 eleq1d
 |-  ( ( A e. V /\ ( x : A -onto-> A /\ y : A -onto-> A ) ) -> ( ( x ( +g ` M ) y ) e. { h | h : A -onto-> A } <-> ( x o. y ) e. { h | h : A -onto-> A } ) )
35 2 19 coex
 |-  ( x o. y ) e. _V
36 foeq1
 |-  ( h = ( x o. y ) -> ( h : A -onto-> A <-> ( x o. y ) : A -onto-> A ) )
37 35 36 elab
 |-  ( ( x o. y ) e. { h | h : A -onto-> A } <-> ( x o. y ) : A -onto-> A )
38 34 37 bitrdi
 |-  ( ( A e. V /\ ( x : A -onto-> A /\ y : A -onto-> A ) ) -> ( ( x ( +g ` M ) y ) e. { h | h : A -onto-> A } <-> ( x o. y ) : A -onto-> A ) )
39 24 38 mpbird
 |-  ( ( A e. V /\ ( x : A -onto-> A /\ y : A -onto-> A ) ) -> ( x ( +g ` M ) y ) e. { h | h : A -onto-> A } )
40 39 ex
 |-  ( A e. V -> ( ( x : A -onto-> A /\ y : A -onto-> A ) -> ( x ( +g ` M ) y ) e. { h | h : A -onto-> A } ) )
41 22 40 syl5bi
 |-  ( A e. V -> ( ( x e. { h | h : A -onto-> A } /\ y e. { h | h : A -onto-> A } ) -> ( x ( +g ` M ) y ) e. { h | h : A -onto-> A } ) )
42 41 ralrimivv
 |-  ( A e. V -> A. x e. { h | h : A -onto-> A } A. y e. { h | h : A -onto-> A } ( x ( +g ` M ) y ) e. { h | h : A -onto-> A } )
43 1 efmndmnd
 |-  ( A e. V -> M e. Mnd )
44 eqid
 |-  ( 0g ` M ) = ( 0g ` M )
45 6 44 31 issubm
 |-  ( M e. Mnd -> ( { h | h : A -onto-> A } e. ( SubMnd ` M ) <-> ( { h | h : A -onto-> A } C_ ( Base ` M ) /\ ( 0g ` M ) e. { h | h : A -onto-> A } /\ A. x e. { h | h : A -onto-> A } A. y e. { h | h : A -onto-> A } ( x ( +g ` M ) y ) e. { h | h : A -onto-> A } ) ) )
46 43 45 syl
 |-  ( A e. V -> ( { h | h : A -onto-> A } e. ( SubMnd ` M ) <-> ( { h | h : A -onto-> A } C_ ( Base ` M ) /\ ( 0g ` M ) e. { h | h : A -onto-> A } /\ A. x e. { h | h : A -onto-> A } A. y e. { h | h : A -onto-> A } ( x ( +g ` M ) y ) e. { h | h : A -onto-> A } ) ) )
47 10 18 42 46 mpbir3and
 |-  ( A e. V -> { h | h : A -onto-> A } e. ( SubMnd ` M ) )