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\in V\to \left\{h|h:A\underset{onto}{⟶}A\right\}\in \mathrm{SubMnd}\left(M\right)$$

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\in \mathrm{V}$$
3		foeq1	$$⊢h=x\to \left(h:A\underset{onto}{⟶}A\leftrightarrow x:A\underset{onto}{⟶}A\right)$$
4	2 3	elab	$$⊢x\in \left\{h|h:A\underset{onto}{⟶}A\right\}\leftrightarrow x:A\underset{onto}{⟶}A$$
5		fof	$$⊢x:A\underset{onto}{⟶}A\to x:A⟶A$$
6		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
7	1 6	elefmndbas	$$⊢A\in V\to \left(x\in {\mathrm{Base}}_M\leftrightarrow x:A⟶A\right)$$
8	5 7	syl5ibr	$$⊢A\in V\to \left(x:A\underset{onto}{⟶}A\to x\in {\mathrm{Base}}_M\right)$$
9	4 8	syl5bi	$$⊢A\in V\to \left(x\in \left\{h|h:A\underset{onto}{⟶}A\right\}\to x\in {\mathrm{Base}}_M\right)$$
10	9	ssrdv	$$⊢A\in V\to \left\{h|h:A\underset{onto}{⟶}A\right\}\subseteq {\mathrm{Base}}_M$$
11	1	efmndid	$$⊢A\in V\to {\mathrm{I}\upharpoonright }_A=0_M$$
12		resiexg	$$⊢A\in V\to {\mathrm{I}\upharpoonright }_A\in \mathrm{V}$$
13		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_A\right):A\underset{1-1\; onto}{⟶}A$$
14		f1ofo	$$⊢\left({\mathrm{I}\upharpoonright }_A\right):A\underset{1-1\; onto}{⟶}A\to \left({\mathrm{I}\upharpoonright }_A\right):A\underset{onto}{⟶}A$$
15	13 14	mp1i	$$⊢A\in V\to \left({\mathrm{I}\upharpoonright }_A\right):A\underset{onto}{⟶}A$$
16		foeq1	$$⊢h={\mathrm{I}\upharpoonright }_A\to \left(h:A\underset{onto}{⟶}A\leftrightarrow \left({\mathrm{I}\upharpoonright }_A\right):A\underset{onto}{⟶}A\right)$$
17	12 15 16	elabd	$$⊢A\in V\to {\mathrm{I}\upharpoonright }_A\in \left\{h|h:A\underset{onto}{⟶}A\right\}$$
18	11 17	eqeltrrd	$$⊢A\in V\to 0_M\in \left\{h|h:A\underset{onto}{⟶}A\right\}$$
19		vex	$$⊢y\in \mathrm{V}$$
20		foeq1	$$⊢h=y\to \left(h:A\underset{onto}{⟶}A\leftrightarrow y:A\underset{onto}{⟶}A\right)$$
21	19 20	elab	$$⊢y\in \left\{h|h:A\underset{onto}{⟶}A\right\}\leftrightarrow y:A\underset{onto}{⟶}A$$
22	4 21	anbi12i	$$⊢\left(x\in \left\{h|h:A\underset{onto}{⟶}A\right\}\wedge y\in \left\{h|h:A\underset{onto}{⟶}A\right\}\right)\leftrightarrow \left(x:A\underset{onto}{⟶}A\wedge y:A\underset{onto}{⟶}A\right)$$
23		foco	$$⊢\left(x:A\underset{onto}{⟶}A\wedge y:A\underset{onto}{⟶}A\right)\to \left(x\circ y\right):A\underset{onto}{⟶}A$$
24	23	adantl	$$⊢\left(A\in V\wedge \left(x:A\underset{onto}{⟶}A\wedge y:A\underset{onto}{⟶}A\right)\right)\to \left(x\circ y\right):A\underset{onto}{⟶}A$$
25		fof	$$⊢y:A\underset{onto}{⟶}A\to y:A⟶A$$
26	5 25	anim12i	$$⊢\left(x:A\underset{onto}{⟶}A\wedge y:A\underset{onto}{⟶}A\right)\to \left(x:A⟶A\wedge y:A⟶A\right)$$
27	1 6	elefmndbas	$$⊢A\in V\to \left(y\in {\mathrm{Base}}_M\leftrightarrow y:A⟶A\right)$$
28	7 27	anbi12d	$$⊢A\in V\to \left(\left(x\in {\mathrm{Base}}_M\wedge y\in {\mathrm{Base}}_M\right)\leftrightarrow \left(x:A⟶A\wedge y:A⟶A\right)\right)$$
29	26 28	syl5ibr	$$⊢A\in V\to \left(\left(x:A\underset{onto}{⟶}A\wedge y:A\underset{onto}{⟶}A\right)\to \left(x\in {\mathrm{Base}}_M\wedge y\in {\mathrm{Base}}_M\right)\right)$$
30	29	imp	$$⊢\left(A\in V\wedge \left(x:A\underset{onto}{⟶}A\wedge y:A\underset{onto}{⟶}A\right)\right)\to \left(x\in {\mathrm{Base}}_M\wedge y\in {\mathrm{Base}}_M\right)$$
31		eqid	$$⊢{+}_M={+}_M$$
32	1 6 31	efmndov	$$⊢\left(x\in {\mathrm{Base}}_M\wedge y\in {\mathrm{Base}}_M\right)\to x{+}_{M}y=x\circ y$$
33	30 32	syl	$$⊢\left(A\in V\wedge \left(x:A\underset{onto}{⟶}A\wedge y:A\underset{onto}{⟶}A\right)\right)\to x{+}_{M}y=x\circ y$$
34	33	eleq1d	$$⊢\left(A\in V\wedge \left(x:A\underset{onto}{⟶}A\wedge y:A\underset{onto}{⟶}A\right)\right)\to \left(x{+}_{M}y\in \left\{h|h:A\underset{onto}{⟶}A\right\}\leftrightarrow x\circ y\in \left\{h|h:A\underset{onto}{⟶}A\right\}\right)$$
35	2 19	coex	$$⊢x\circ y\in \mathrm{V}$$
36		foeq1	$$⊢h=x\circ y\to \left(h:A\underset{onto}{⟶}A\leftrightarrow \left(x\circ y\right):A\underset{onto}{⟶}A\right)$$
37	35 36	elab	$$⊢x\circ y\in \left\{h|h:A\underset{onto}{⟶}A\right\}\leftrightarrow \left(x\circ y\right):A\underset{onto}{⟶}A$$
38	34 37	bitrdi	$$⊢\left(A\in V\wedge \left(x:A\underset{onto}{⟶}A\wedge y:A\underset{onto}{⟶}A\right)\right)\to \left(x{+}_{M}y\in \left\{h|h:A\underset{onto}{⟶}A\right\}\leftrightarrow \left(x\circ y\right):A\underset{onto}{⟶}A\right)$$
39	24 38	mpbird	$$⊢\left(A\in V\wedge \left(x:A\underset{onto}{⟶}A\wedge y:A\underset{onto}{⟶}A\right)\right)\to x{+}_{M}y\in \left\{h|h:A\underset{onto}{⟶}A\right\}$$
40	39	ex	$$⊢A\in V\to \left(\left(x:A\underset{onto}{⟶}A\wedge y:A\underset{onto}{⟶}A\right)\to x{+}_{M}y\in \left\{h|h:A\underset{onto}{⟶}A\right\}\right)$$
41	22 40	syl5bi	$$⊢A\in V\to \left(\left(x\in \left\{h|h:A\underset{onto}{⟶}A\right\}\wedge y\in \left\{h|h:A\underset{onto}{⟶}A\right\}\right)\to x{+}_{M}y\in \left\{h|h:A\underset{onto}{⟶}A\right\}\right)$$
42	41	ralrimivv	$$⊢A\in V\to \forall x\in \left\{h|h:A\underset{onto}{⟶}A\right\}\forall y\in \left\{h|h:A\underset{onto}{⟶}A\right\}x{+}_{M}y\in \left\{h|h:A\underset{onto}{⟶}A\right\}$$
43	1	efmndmnd	$$⊢A\in V\to M\in \mathrm{Mnd}$$
44		eqid	$$⊢0_M=0_M$$
45	6 44 31	issubm	$$⊢M\in \mathrm{Mnd}\to \left(\left\{h|h:A\underset{onto}{⟶}A\right\}\in \mathrm{SubMnd}\left(M\right)\leftrightarrow \left(\left\{h|h:A\underset{onto}{⟶}A\right\}\subseteq {\mathrm{Base}}_M\wedge 0_M\in \left\{h|h:A\underset{onto}{⟶}A\right\}\wedge \forall x\in \left\{h|h:A\underset{onto}{⟶}A\right\}\forall y\in \left\{h|h:A\underset{onto}{⟶}A\right\}x{+}_{M}y\in \left\{h|h:A\underset{onto}{⟶}A\right\}\right)\right)$$
46	43 45	syl	$$⊢A\in V\to \left(\left\{h|h:A\underset{onto}{⟶}A\right\}\in \mathrm{SubMnd}\left(M\right)\leftrightarrow \left(\left\{h|h:A\underset{onto}{⟶}A\right\}\subseteq {\mathrm{Base}}_M\wedge 0_M\in \left\{h|h:A\underset{onto}{⟶}A\right\}\wedge \forall x\in \left\{h|h:A\underset{onto}{⟶}A\right\}\forall y\in \left\{h|h:A\underset{onto}{⟶}A\right\}x{+}_{M}y\in \left\{h|h:A\underset{onto}{⟶}A\right\}\right)\right)$$
47	10 18 42 46	mpbir3and	$$⊢A\in V\to \left\{h|h:A\underset{onto}{⟶}A\right\}\in \mathrm{SubMnd}\left(M\right)$$