Metamath Proof Explorer


Theorem injsubmefmnd

Description: The set of injective 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 injsubmefmnd A V h | h : A 1-1 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 f1eq1 h = x h : A 1-1 A x : A 1-1 A
4 2 3 elab x h | h : A 1-1 A x : A 1-1 A
5 f1f x : A 1-1 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 1-1 A x Base M
9 4 8 syl5bi A V x h | h : A 1-1 A x Base M
10 9 ssrdv A V h | h : A 1-1 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 f1of1 I A : A 1-1 onto A I A : A 1-1 A
15 13 14 mp1i A V I A : A 1-1 A
16 f1eq1 h = I A h : A 1-1 A I A : A 1-1 A
17 12 15 16 elabd A V I A h | h : A 1-1 A
18 11 17 eqeltrrd A V 0 M h | h : A 1-1 A
19 vex y V
20 f1eq1 h = y h : A 1-1 A y : A 1-1 A
21 19 20 elab y h | h : A 1-1 A y : A 1-1 A
22 4 21 anbi12i x h | h : A 1-1 A y h | h : A 1-1 A x : A 1-1 A y : A 1-1 A
23 f1co x : A 1-1 A y : A 1-1 A x y : A 1-1 A
24 23 adantl A V x : A 1-1 A y : A 1-1 A x y : A 1-1 A
25 f1f y : A 1-1 A y : A A
26 5 25 anim12i x : A 1-1 A y : A 1-1 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 1-1 A y : A 1-1 A x Base M y Base M
30 29 imp A V x : A 1-1 A y : A 1-1 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 1-1 A y : A 1-1 A x + M y = x y
34 33 eleq1d A V x : A 1-1 A y : A 1-1 A x + M y h | h : A 1-1 A x y h | h : A 1-1 A
35 2 19 coex x y V
36 f1eq1 h = x y h : A 1-1 A x y : A 1-1 A
37 35 36 elab x y h | h : A 1-1 A x y : A 1-1 A
38 34 37 bitrdi A V x : A 1-1 A y : A 1-1 A x + M y h | h : A 1-1 A x y : A 1-1 A
39 24 38 mpbird A V x : A 1-1 A y : A 1-1 A x + M y h | h : A 1-1 A
40 39 ex A V x : A 1-1 A y : A 1-1 A x + M y h | h : A 1-1 A
41 22 40 syl5bi A V x h | h : A 1-1 A y h | h : A 1-1 A x + M y h | h : A 1-1 A
42 41 ralrimivv A V x h | h : A 1-1 A y h | h : A 1-1 A x + M y h | h : A 1-1 A
43 1 efmndmnd A V M Mnd
44 eqid 0 M = 0 M
45 6 44 31 issubm M Mnd h | h : A 1-1 A SubMnd M h | h : A 1-1 A Base M 0 M h | h : A 1-1 A x h | h : A 1-1 A y h | h : A 1-1 A x + M y h | h : A 1-1 A
46 43 45 syl A V h | h : A 1-1 A SubMnd M h | h : A 1-1 A Base M 0 M h | h : A 1-1 A x h | h : A 1-1 A y h | h : A 1-1 A x + M y h | h : A 1-1 A
47 10 18 42 46 mpbir3and A V h | h : A 1-1 A SubMnd M