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