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

Metamath Proof Explorer

Theorem smndex1bas

Description: The base set of the monoid of endofunctions on NN0 restricted to the modulo function I and the constant functions ( GK ) . (Contributed by AV, 12-Feb-2024)

Ref Expression
Hypotheses smndex1ibas.m ⊢ M = EndoFMnd ⁡ ℕ 0
smndex1ibas.n ⊢ N ∈ ℕ
smndex1ibas.i ⊢ I = x ∈ ℕ 0 ⟼ x mod N
smndex1ibas.g ⊢ G = n ∈ 0 ..^ N ⟼ x ∈ ℕ 0 ⟼ n
smndex1mgm.b ⊢ B = I ∪ ⋃ n ∈ 0 ..^ N G ⁡ n
smndex1mgm.s ⊢ S = M ↾ 𝑠 B
Assertion smndex1bas ⊢ Base S = B

Proof

Step Hyp Ref Expression
1 smndex1ibas.m ⊢ M = EndoFMnd ⁡ ℕ 0
2 smndex1ibas.n ⊢ N ∈ ℕ
3 smndex1ibas.i ⊢ I = x ∈ ℕ 0 ⟼ x mod N
4 smndex1ibas.g ⊢ G = n ∈ 0 ..^ N ⟼ x ∈ ℕ 0 ⟼ n
5 smndex1mgm.b ⊢ B = I ∪ ⋃ n ∈ 0 ..^ N G ⁡ n
6 smndex1mgm.s ⊢ S = M ↾ 𝑠 B
7 1 2 3 4 5 smndex1basss ⊢ B ⊆ Base M
8 dfss ⊢ B ⊆ Base M ↔ B = B ∩ Base M
9 7 8 mpbi ⊢ B = B ∩ Base M
10 snex ⊢ I ∈ V
11 ovex ⊢ 0 ..^ N ∈ V
12 snex ⊢ G ⁡ n ∈ V
13 11 12 iunex ⊢ ⋃ n ∈ 0 ..^ N G ⁡ n ∈ V
14 10 13 unex ⊢ I ∪ ⋃ n ∈ 0 ..^ N G ⁡ n ∈ V
15 5 14 eqeltri ⊢ B ∈ V
16 eqid ⊢ Base M = Base M
17 6 16 ressbas ⊢ B ∈ V → B ∩ Base M = Base S
18 15 17 ax-mp ⊢ B ∩ Base M = Base S
19 9 18 eqtr2i ⊢ Base S = B