This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑀 ) ∉ 𝐵