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 No typesetting found for |- M = ( EndoFMnd ` A ) with typecode |-
Assertion sursubmefmnd A V h | h : A onto A SubMnd M

Proof

Step Hyp Ref Expression
1 sursubmefmnd.m Could not format M = ( EndoFMnd ` A ) : No typesetting found for |- M = ( EndoFMnd ` A ) with typecode |-
2 vex x V
3 foeq1 h = x h : A onto A x : A onto A
4 2 3 elab x 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 V x Base M x : A A
8 5 7 syl5ibr A V x : A onto A x Base M
9 4 8 syl5bi A V x h | h : A onto A x Base M
10 9 ssrdv A V h | h : A onto A Base M
11 1 efmndid A V I A = 0 M
12 resiexg A V I A 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 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 V I A h | h : A onto A
18 11 17 eqeltrrd A V 0 M h | h : A onto A
19 vex y V
20 foeq1 h = y h : A onto A y : A onto A
21 19 20 elab y h | h : A onto A y : A onto A
22 4 21 anbi12i x h | h : A onto A y h | h : A onto A x : A onto A y : A onto A
23 foco x : A onto A y : A onto A x y : A onto A
24 23 adantl A V x : A onto A y : A onto A x 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 V y Base M y : A A
28 7 27 anbi12d A V x Base M y Base M x : A A y : A A
29 26 28 syl5ibr A V x : A onto A y : A onto A x Base M y Base M
30 29 imp A V x : A onto A y : A onto A x Base M y Base M
31 eqid + M = + M
32 1 6 31 efmndov x Base M y Base M x + M y = x y
33 30 32 syl A V x : A onto A y : A onto A x + M y = x y
34 33 eleq1d A V x : A onto A y : A onto A x + M y h | h : A onto A x y h | h : A onto A
35 2 19 coex x y V
36 foeq1 h = x y h : A onto A x y : A onto A
37 35 36 elab x y h | h : A onto A x y : A onto A
38 34 37 bitrdi A V x : A onto A y : A onto A x + M y h | h : A onto A x y : A onto A
39 24 38 mpbird A V x : A onto A y : A onto A x + M y h | h : A onto A
40 39 ex A V x : A onto A y : A onto A x + M y h | h : A onto A
41 22 40 syl5bi A V x h | h : A onto A y h | h : A onto A x + M y h | h : A onto A
42 41 ralrimivv A V x h | h : A onto A y h | h : A onto A x + M y h | h : A onto A
43 1 efmndmnd A V M Mnd
44 eqid 0 M = 0 M
45 6 44 31 issubm M Mnd h | h : A onto A SubMnd M h | h : A onto A Base M 0 M h | h : A onto A x h | h : A onto A y h | h : A onto A x + M y h | h : A onto A
46 43 45 syl A V h | h : A onto A SubMnd M h | h : A onto A Base M 0 M h | h : A onto A x h | h : A onto A y h | h : A onto A x + M y h | h : A onto A
47 10 18 42 46 mpbir3and A V h | h : A onto A SubMnd M