Theorem smndex1n0mnd

Description: The identity of the monoid M of endofunctions on set NN0 is not contained in the base set of the constructed monoid S . (Contributed by AV, 17-Feb-2024)

	Ref	Expression
Hypotheses	smndex1ibas.m	$$⊢M=\mathrm{EndoFMnd}\left({\mathbb{N}}_0\right)$$
	smndex1ibas.n	$$⊢N\in \mathbb{N}$$
	smndex1ibas.i	$$⊢I=\left(x\in {\mathbb{N}}_0⟼x\mathrm{mod}N\right)$$
	smndex1ibas.g	$$⊢G=\left(n\in \left(0..^N\right)⟼\left(x\in {\mathbb{N}}_0⟼n\right)\right)$$
	smndex1mgm.b	$$⊢B=\left\{I\right\}\cup \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}$$
	smndex1mgm.s	$$⊢S=M{\upharpoonright }_{𝑠}B$$
Assertion	smndex1n0mnd	$$⊢0_M\notin B$$

Proof

Step	Hyp	Ref	Expression
1		smndex1ibas.m	$$⊢M=\mathrm{EndoFMnd}\left({\mathbb{N}}_0\right)$$
2		smndex1ibas.n	$$⊢N\in \mathbb{N}$$
3		smndex1ibas.i	$$⊢I=\left(x\in {\mathbb{N}}_0⟼x\mathrm{mod}N\right)$$
4		smndex1ibas.g	$$⊢G=\left(n\in \left(0..^N\right)⟼\left(x\in {\mathbb{N}}_0⟼n\right)\right)$$
5		smndex1mgm.b	$$⊢B=\left\{I\right\}\cup \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}$$
6		smndex1mgm.s	$$⊢S=M{\upharpoonright }_{𝑠}B$$
7		nnnn0	$$⊢N\in \mathbb{N}\to N\in {\mathbb{N}}_0$$
8		fveq2	$$⊢x=N\to \left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(x\right)=\left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(N\right)$$
9	2 7	ax-mp	$$⊢N\in {\mathbb{N}}_0$$
10		fvresi	$$⊢N\in {\mathbb{N}}_0\to \left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(N\right)=N$$
11	9 10	ax-mp	$$⊢\left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(N\right)=N$$
12	8 11	eqtrdi	$$⊢x=N\to \left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(x\right)=N$$
13		fveq2	$$⊢x=N\to I\left(x\right)=I\left(N\right)$$
14	12 13	eqeq12d	$$⊢x=N\to \left(\left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(x\right)=I\left(x\right)\leftrightarrow N=I\left(N\right)\right)$$
15	14	notbid	$$⊢x=N\to \left(\neg \left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(x\right)=I\left(x\right)\leftrightarrow \neg N=I\left(N\right)\right)$$
16	15	adantl	$$⊢\left(N\in \mathbb{N}\wedge x=N\right)\to \left(\neg \left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(x\right)=I\left(x\right)\leftrightarrow \neg N=I\left(N\right)\right)$$
17		nnne0	$$⊢N\in \mathbb{N}\to N\ne 0$$
18	17	neneqd	$$⊢N\in \mathbb{N}\to \neg N=0$$
19		oveq1	$$⊢x=N\to x\mathrm{mod}N=N\mathrm{mod}N$$
20		nnrp	$$⊢N\in \mathbb{N}\to N\in {ℝ}^{+}$$
21		modid0	$$⊢N\in {ℝ}^{+}\to N\mathrm{mod}N=0$$
22	20 21	syl	$$⊢N\in \mathbb{N}\to N\mathrm{mod}N=0$$
23	19 22	sylan9eqr	$$⊢\left(N\in \mathbb{N}\wedge x=N\right)\to x\mathrm{mod}N=0$$
24		c0ex	$$⊢0\in \mathrm{V}$$
25	24	a1i	$$⊢N\in \mathbb{N}\to 0\in \mathrm{V}$$
26	3 23 7 25	fvmptd2	$$⊢N\in \mathbb{N}\to I\left(N\right)=0$$
27	26	eqeq2d	$$⊢N\in \mathbb{N}\to \left(N=I\left(N\right)\leftrightarrow N=0\right)$$
28	18 27	mtbird	$$⊢N\in \mathbb{N}\to \neg N=I\left(N\right)$$
29	7 16 28	rspcedvd	$$⊢N\in \mathbb{N}\to \exists x\in {\mathbb{N}}_0\neg \left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(x\right)=I\left(x\right)$$
30	2 29	ax-mp	$$⊢\exists x\in {\mathbb{N}}_0\neg \left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(x\right)=I\left(x\right)$$
31		rexnal	$$⊢\exists x\in {\mathbb{N}}_0\neg \left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(x\right)=I\left(x\right)\leftrightarrow \neg \forall x\in {\mathbb{N}}_0\left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(x\right)=I\left(x\right)$$
32	30 31	mpbi	$$⊢\neg \forall x\in {\mathbb{N}}_0\left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(x\right)=I\left(x\right)$$
33		fnresi	$$⊢\left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)Fn{\mathbb{N}}_0$$
34		ovex	$$⊢x\mathrm{mod}N\in \mathrm{V}$$
35	34 3	fnmpti	$$⊢IFn{\mathbb{N}}_0$$
36		eqfnfv	$$⊢\left(\left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)Fn{\mathbb{N}}_0\wedge IFn{\mathbb{N}}_0\right)\to \left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=I\leftrightarrow \forall x\in {\mathbb{N}}_0\left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(x\right)=I\left(x\right)\right)$$
37	33 35 36	mp2an	$$⊢{\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=I\leftrightarrow \forall x\in {\mathbb{N}}_0\left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(x\right)=I\left(x\right)$$
38	32 37	mtbir	$$⊢\neg {\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=I$$
39	9	a1i	$$⊢n\in \left(0..^N\right)\to N\in {\mathbb{N}}_0$$
40		fveq2	$$⊢x=N\to G\left(n\right)\left(x\right)=G\left(n\right)\left(N\right)$$
41	12 40	eqeq12d	$$⊢x=N\to \left(\left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(x\right)=G\left(n\right)\left(x\right)\leftrightarrow N=G\left(n\right)\left(N\right)\right)$$
42	41	notbid	$$⊢x=N\to \left(\neg \left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(x\right)=G\left(n\right)\left(x\right)\leftrightarrow \neg N=G\left(n\right)\left(N\right)\right)$$
43	42	adantl	$$⊢\left(n\in \left(0..^N\right)\wedge x=N\right)\to \left(\neg \left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(x\right)=G\left(n\right)\left(x\right)\leftrightarrow \neg N=G\left(n\right)\left(N\right)\right)$$
44		fzonel	$$⊢\neg N\in \left(0..^N\right)$$
45		eleq1	$$⊢n=N\to \left(n\in \left(0..^N\right)\leftrightarrow N\in \left(0..^N\right)\right)$$
46	45	eqcoms	$$⊢N=n\to \left(n\in \left(0..^N\right)\leftrightarrow N\in \left(0..^N\right)\right)$$
47	44 46	mtbiri	$$⊢N=n\to \neg n\in \left(0..^N\right)$$
48	47	con2i	$$⊢n\in \left(0..^N\right)\to \neg N=n$$
49		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
50	49	mptex	$$⊢\left(x\in {\mathbb{N}}_0⟼n\right)\in \mathrm{V}$$
51	4	fvmpt2	$$⊢\left(n\in \left(0..^N\right)\wedge \left(x\in {\mathbb{N}}_0⟼n\right)\in \mathrm{V}\right)\to G\left(n\right)=\left(x\in {\mathbb{N}}_0⟼n\right)$$
52	50 51	mpan2	$$⊢n\in \left(0..^N\right)\to G\left(n\right)=\left(x\in {\mathbb{N}}_0⟼n\right)$$
53		eqidd	$$⊢\left(n\in \left(0..^N\right)\wedge x=N\right)\to n=n$$
54		id	$$⊢n\in \left(0..^N\right)\to n\in \left(0..^N\right)$$
55	52 53 39 54	fvmptd	$$⊢n\in \left(0..^N\right)\to G\left(n\right)\left(N\right)=n$$
56	55	eqeq2d	$$⊢n\in \left(0..^N\right)\to \left(N=G\left(n\right)\left(N\right)\leftrightarrow N=n\right)$$
57	48 56	mtbird	$$⊢n\in \left(0..^N\right)\to \neg N=G\left(n\right)\left(N\right)$$
58	39 43 57	rspcedvd	$$⊢n\in \left(0..^N\right)\to \exists x\in {\mathbb{N}}_0\neg \left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(x\right)=G\left(n\right)\left(x\right)$$
59		rexnal	$$⊢\exists x\in {\mathbb{N}}_0\neg \left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(x\right)=G\left(n\right)\left(x\right)\leftrightarrow \neg \forall x\in {\mathbb{N}}_0\left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(x\right)=G\left(n\right)\left(x\right)$$
60	58 59	sylib	$$⊢n\in \left(0..^N\right)\to \neg \forall x\in {\mathbb{N}}_0\left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(x\right)=G\left(n\right)\left(x\right)$$
61		vex	$$⊢n\in \mathrm{V}$$
62		eqid	$$⊢\left(x\in {\mathbb{N}}_0⟼n\right)=\left(x\in {\mathbb{N}}_0⟼n\right)$$
63	61 62	fnmpti	$$⊢\left(x\in {\mathbb{N}}_0⟼n\right)Fn{\mathbb{N}}_0$$
64	52	fneq1d	$$⊢n\in \left(0..^N\right)\to \left(G\left(n\right)Fn{\mathbb{N}}_0\leftrightarrow \left(x\in {\mathbb{N}}_0⟼n\right)Fn{\mathbb{N}}_0\right)$$
65	63 64	mpbiri	$$⊢n\in \left(0..^N\right)\to G\left(n\right)Fn{\mathbb{N}}_0$$
66		eqfnfv	$$⊢\left(\left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)Fn{\mathbb{N}}_0\wedge G\left(n\right)Fn{\mathbb{N}}_0\right)\to \left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=G\left(n\right)\leftrightarrow \forall x\in {\mathbb{N}}_0\left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(x\right)=G\left(n\right)\left(x\right)\right)$$
67	33 65 66	sylancr	$$⊢n\in \left(0..^N\right)\to \left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=G\left(n\right)\leftrightarrow \forall x\in {\mathbb{N}}_0\left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(x\right)=G\left(n\right)\left(x\right)\right)$$
68	60 67	mtbird	$$⊢n\in \left(0..^N\right)\to \neg {\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=G\left(n\right)$$
69	68	nrex	$$⊢\neg \exists n\in \left(0..^N\right){\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=G\left(n\right)$$
70	38 69	pm3.2ni	$$⊢\neg \left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=I\vee \exists n\in \left(0..^N\right){\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=G\left(n\right)\right)$$
71	1	efmndid	$$⊢{\mathbb{N}}_0\in \mathrm{V}\to {\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=0_M$$
72	49 71	ax-mp	$$⊢{\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=0_M$$
73	72	eqcomi	$$⊢0_M={\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}$$
74	73 5	eleq12i	$$⊢0_M\in B\leftrightarrow {\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\in \left(\left\{I\right\}\cup \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\right)$$
75		elun	$$⊢{\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\in \left(\left\{I\right\}\cup \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\right)\leftrightarrow \left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\in \left\{I\right\}\vee {\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\in \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\right)$$
76		resiexg	$$⊢{\mathbb{N}}_0\in \mathrm{V}\to {\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\in \mathrm{V}$$
77	49 76	ax-mp	$$⊢{\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\in \mathrm{V}$$
78	77	elsn	$$⊢{\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\in \left\{I\right\}\leftrightarrow {\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=I$$
79		eliun	$$⊢{\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\in \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\leftrightarrow \exists n\in \left(0..^N\right){\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\in \left\{G\left(n\right)\right\}$$
80	77	elsn	$$⊢{\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\in \left\{G\left(n\right)\right\}\leftrightarrow {\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=G\left(n\right)$$
81	80	rexbii	$$⊢\exists n\in \left(0..^N\right){\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\in \left\{G\left(n\right)\right\}\leftrightarrow \exists n\in \left(0..^N\right){\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=G\left(n\right)$$
82	79 81	bitri	$$⊢{\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\in \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\leftrightarrow \exists n\in \left(0..^N\right){\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=G\left(n\right)$$
83	78 82	orbi12i	$$⊢\left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\in \left\{I\right\}\vee {\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\in \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\right)\leftrightarrow \left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=I\vee \exists n\in \left(0..^N\right){\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=G\left(n\right)\right)$$
84	75 83	bitri	$$⊢{\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}\in \left(\left\{I\right\}\cup \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\right)\leftrightarrow \left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=I\vee \exists n\in \left(0..^N\right){\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=G\left(n\right)\right)$$
85	74 84	bitri	$$⊢0_M\in B\leftrightarrow \left({\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=I\vee \exists n\in \left(0..^N\right){\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=G\left(n\right)\right)$$
86	70 85	mtbir	$$⊢\neg 0_M\in B$$
87	86	nelir	$$⊢0_M\notin B$$