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	⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
	smndex1ibas.n	⊢ 𝑁 ∈ ℕ
	smndex1ibas.i	⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
	smndex1ibas.g	⊢ 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
	smndex1mgm.b	⊢ 𝐵 = ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } )
	smndex1mgm.s	⊢ 𝑆 = ( 𝑀 ↾s 𝐵 )
Assertion	smndex1n0mnd	⊢ ( 0g ‘ 𝑀 ) ∉ 𝐵

Proof

Step	Hyp	Ref	Expression
1		smndex1ibas.m	⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
2		smndex1ibas.n	⊢ 𝑁 ∈ ℕ
3		smndex1ibas.i	⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
4		smndex1ibas.g	⊢ 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
5		smndex1mgm.b	⊢ 𝐵 = ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } )
6		smndex1mgm.s	⊢ 𝑆 = ( 𝑀 ↾s 𝐵 )
7		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
8		fveq2	⊢ ( 𝑥 = 𝑁 → ( ( I ↾ ℕ0 ) ‘ 𝑥 ) = ( ( I ↾ ℕ0 ) ‘ 𝑁 ) )
9	2 7	ax-mp	⊢ 𝑁 ∈ ℕ0
10		fvresi	⊢ ( 𝑁 ∈ ℕ0 → ( ( I ↾ ℕ0 ) ‘ 𝑁 ) = 𝑁 )
11	9 10	ax-mp	⊢ ( ( I ↾ ℕ0 ) ‘ 𝑁 ) = 𝑁
12	8 11	eqtrdi	⊢ ( 𝑥 = 𝑁 → ( ( I ↾ ℕ0 ) ‘ 𝑥 ) = 𝑁 )
13		fveq2	⊢ ( 𝑥 = 𝑁 → ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑁 ) )
14	12 13	eqeq12d	⊢ ( 𝑥 = 𝑁 → ( ( ( I ↾ ℕ0 ) ‘ 𝑥 ) = ( 𝐼 ‘ 𝑥 ) ↔ 𝑁 = ( 𝐼 ‘ 𝑁 ) ) )
15	14	notbid	⊢ ( 𝑥 = 𝑁 → ( ¬ ( ( I ↾ ℕ0 ) ‘ 𝑥 ) = ( 𝐼 ‘ 𝑥 ) ↔ ¬ 𝑁 = ( 𝐼 ‘ 𝑁 ) ) )
16	15	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 = 𝑁 ) → ( ¬ ( ( I ↾ ℕ0 ) ‘ 𝑥 ) = ( 𝐼 ‘ 𝑥 ) ↔ ¬ 𝑁 = ( 𝐼 ‘ 𝑁 ) ) )
17		nnne0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
18	17	neneqd	⊢ ( 𝑁 ∈ ℕ → ¬ 𝑁 = 0 )
19		oveq1	⊢ ( 𝑥 = 𝑁 → ( 𝑥 mod 𝑁 ) = ( 𝑁 mod 𝑁 ) )
20		nnrp	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
21		modid0	⊢ ( 𝑁 ∈ ℝ+ → ( 𝑁 mod 𝑁 ) = 0 )
22	20 21	syl	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 mod 𝑁 ) = 0 )
23	19 22	sylan9eqr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 = 𝑁 ) → ( 𝑥 mod 𝑁 ) = 0 )
24		c0ex	⊢ 0 ∈ V
25	24	a1i	⊢ ( 𝑁 ∈ ℕ → 0 ∈ V )
26	3 23 7 25	fvmptd2	⊢ ( 𝑁 ∈ ℕ → ( 𝐼 ‘ 𝑁 ) = 0 )
27	26	eqeq2d	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 = ( 𝐼 ‘ 𝑁 ) ↔ 𝑁 = 0 ) )
28	18 27	mtbird	⊢ ( 𝑁 ∈ ℕ → ¬ 𝑁 = ( 𝐼 ‘ 𝑁 ) )
29	7 16 28	rspcedvd	⊢ ( 𝑁 ∈ ℕ → ∃ 𝑥 ∈ ℕ0 ¬ ( ( I ↾ ℕ0 ) ‘ 𝑥 ) = ( 𝐼 ‘ 𝑥 ) )
30	2 29	ax-mp	⊢ ∃ 𝑥 ∈ ℕ0 ¬ ( ( I ↾ ℕ0 ) ‘ 𝑥 ) = ( 𝐼 ‘ 𝑥 )
31		rexnal	⊢ ( ∃ 𝑥 ∈ ℕ0 ¬ ( ( I ↾ ℕ0 ) ‘ 𝑥 ) = ( 𝐼 ‘ 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ ℕ0 ( ( I ↾ ℕ0 ) ‘ 𝑥 ) = ( 𝐼 ‘ 𝑥 ) )
32	30 31	mpbi	⊢ ¬ ∀ 𝑥 ∈ ℕ0 ( ( I ↾ ℕ0 ) ‘ 𝑥 ) = ( 𝐼 ‘ 𝑥 )
33		fnresi	⊢ ( I ↾ ℕ0 ) Fn ℕ0
34		ovex	⊢ ( 𝑥 mod 𝑁 ) ∈ V
35	34 3	fnmpti	⊢ 𝐼 Fn ℕ0
36		eqfnfv	⊢ ( ( ( I ↾ ℕ0 ) Fn ℕ0 ∧ 𝐼 Fn ℕ0 ) → ( ( I ↾ ℕ0 ) = 𝐼 ↔ ∀ 𝑥 ∈ ℕ0 ( ( I ↾ ℕ0 ) ‘ 𝑥 ) = ( 𝐼 ‘ 𝑥 ) ) )
37	33 35 36	mp2an	⊢ ( ( I ↾ ℕ0 ) = 𝐼 ↔ ∀ 𝑥 ∈ ℕ0 ( ( I ↾ ℕ0 ) ‘ 𝑥 ) = ( 𝐼 ‘ 𝑥 ) )
38	32 37	mtbir	⊢ ¬ ( I ↾ ℕ0 ) = 𝐼
39	9	a1i	⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → 𝑁 ∈ ℕ0 )
40		fveq2	⊢ ( 𝑥 = 𝑁 → ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑁 ) )
41	12 40	eqeq12d	⊢ ( 𝑥 = 𝑁 → ( ( ( I ↾ ℕ0 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) ↔ 𝑁 = ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑁 ) ) )
42	41	notbid	⊢ ( 𝑥 = 𝑁 → ( ¬ ( ( I ↾ ℕ0 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) ↔ ¬ 𝑁 = ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑁 ) ) )
43	42	adantl	⊢ ( ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 = 𝑁 ) → ( ¬ ( ( I ↾ ℕ0 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) ↔ ¬ 𝑁 = ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑁 ) ) )
44		fzonel	⊢ ¬ 𝑁 ∈ ( 0 ..^ 𝑁 )
45		eleq1	⊢ ( 𝑛 = 𝑁 → ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑁 ∈ ( 0 ..^ 𝑁 ) ) )
46	45	eqcoms	⊢ ( 𝑁 = 𝑛 → ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑁 ∈ ( 0 ..^ 𝑁 ) ) )
47	44 46	mtbiri	⊢ ( 𝑁 = 𝑛 → ¬ 𝑛 ∈ ( 0 ..^ 𝑁 ) )
48	47	con2i	⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → ¬ 𝑁 = 𝑛 )
49		nn0ex	⊢ ℕ0 ∈ V
50	49	mptex	⊢ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) ∈ V
51	4	fvmpt2	⊢ ( ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) ∈ V ) → ( 𝐺 ‘ 𝑛 ) = ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
52	50 51	mpan2	⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝑛 ) = ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
53		eqidd	⊢ ( ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 = 𝑁 ) → 𝑛 = 𝑛 )
54		id	⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → 𝑛 ∈ ( 0 ..^ 𝑁 ) )
55	52 53 39 54	fvmptd	⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑁 ) = 𝑛 )
56	55	eqeq2d	⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → ( 𝑁 = ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑁 ) ↔ 𝑁 = 𝑛 ) )
57	48 56	mtbird	⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → ¬ 𝑁 = ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑁 ) )
58	39 43 57	rspcedvd	⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → ∃ 𝑥 ∈ ℕ0 ¬ ( ( I ↾ ℕ0 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) )
59		rexnal	⊢ ( ∃ 𝑥 ∈ ℕ0 ¬ ( ( I ↾ ℕ0 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ ℕ0 ( ( I ↾ ℕ0 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) )
60	58 59	sylib	⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → ¬ ∀ 𝑥 ∈ ℕ0 ( ( I ↾ ℕ0 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) )
61		vex	⊢ 𝑛 ∈ V
62		eqid	⊢ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑥 ∈ ℕ0 ↦ 𝑛 )
63	61 62	fnmpti	⊢ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) Fn ℕ0
64	52	fneq1d	⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝐺 ‘ 𝑛 ) Fn ℕ0 ↔ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) Fn ℕ0 ) )
65	63 64	mpbiri	⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝑛 ) Fn ℕ0 )
66		eqfnfv	⊢ ( ( ( I ↾ ℕ0 ) Fn ℕ0 ∧ ( 𝐺 ‘ 𝑛 ) Fn ℕ0 ) → ( ( I ↾ ℕ0 ) = ( 𝐺 ‘ 𝑛 ) ↔ ∀ 𝑥 ∈ ℕ0 ( ( I ↾ ℕ0 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) ) )
67	33 65 66	sylancr	⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → ( ( I ↾ ℕ0 ) = ( 𝐺 ‘ 𝑛 ) ↔ ∀ 𝑥 ∈ ℕ0 ( ( I ↾ ℕ0 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) ) )
68	60 67	mtbird	⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → ¬ ( I ↾ ℕ0 ) = ( 𝐺 ‘ 𝑛 ) )
69	68	nrex	⊢ ¬ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) ( I ↾ ℕ0 ) = ( 𝐺 ‘ 𝑛 )
70	38 69	pm3.2ni	⊢ ¬ ( ( I ↾ ℕ0 ) = 𝐼 ∨ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) ( I ↾ ℕ0 ) = ( 𝐺 ‘ 𝑛 ) )
71	1	efmndid	⊢ ( ℕ0 ∈ V → ( I ↾ ℕ0 ) = ( 0g ‘ 𝑀 ) )
72	49 71	ax-mp	⊢ ( I ↾ ℕ0 ) = ( 0g ‘ 𝑀 )
73	72	eqcomi	⊢ ( 0g ‘ 𝑀 ) = ( I ↾ ℕ0 )
74	73 5	eleq12i	⊢ ( ( 0g ‘ 𝑀 ) ∈ 𝐵 ↔ ( I ↾ ℕ0 ) ∈ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) )
75		elun	⊢ ( ( I ↾ ℕ0 ) ∈ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) ↔ ( ( I ↾ ℕ0 ) ∈ { 𝐼 } ∨ ( I ↾ ℕ0 ) ∈ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) )
76		resiexg	⊢ ( ℕ0 ∈ V → ( I ↾ ℕ0 ) ∈ V )
77	49 76	ax-mp	⊢ ( I ↾ ℕ0 ) ∈ V
78	77	elsn	⊢ ( ( I ↾ ℕ0 ) ∈ { 𝐼 } ↔ ( I ↾ ℕ0 ) = 𝐼 )
79		eliun	⊢ ( ( I ↾ ℕ0 ) ∈ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ↔ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) ( I ↾ ℕ0 ) ∈ { ( 𝐺 ‘ 𝑛 ) } )
80	77	elsn	⊢ ( ( I ↾ ℕ0 ) ∈ { ( 𝐺 ‘ 𝑛 ) } ↔ ( I ↾ ℕ0 ) = ( 𝐺 ‘ 𝑛 ) )
81	80	rexbii	⊢ ( ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) ( I ↾ ℕ0 ) ∈ { ( 𝐺 ‘ 𝑛 ) } ↔ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) ( I ↾ ℕ0 ) = ( 𝐺 ‘ 𝑛 ) )
82	79 81	bitri	⊢ ( ( I ↾ ℕ0 ) ∈ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ↔ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) ( I ↾ ℕ0 ) = ( 𝐺 ‘ 𝑛 ) )
83	78 82	orbi12i	⊢ ( ( ( I ↾ ℕ0 ) ∈ { 𝐼 } ∨ ( I ↾ ℕ0 ) ∈ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) ↔ ( ( I ↾ ℕ0 ) = 𝐼 ∨ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) ( I ↾ ℕ0 ) = ( 𝐺 ‘ 𝑛 ) ) )
84	75 83	bitri	⊢ ( ( I ↾ ℕ0 ) ∈ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) ↔ ( ( I ↾ ℕ0 ) = 𝐼 ∨ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) ( I ↾ ℕ0 ) = ( 𝐺 ‘ 𝑛 ) ) )
85	74 84	bitri	⊢ ( ( 0g ‘ 𝑀 ) ∈ 𝐵 ↔ ( ( I ↾ ℕ0 ) = 𝐼 ∨ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) ( I ↾ ℕ0 ) = ( 𝐺 ‘ 𝑛 ) ) )
86	70 85	mtbir	⊢ ¬ ( 0g ‘ 𝑀 ) ∈ 𝐵
87	86	nelir	⊢ ( 0g ‘ 𝑀 ) ∉ 𝐵