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

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 1 2 3 4 5 smndex1basss ⊢ 𝐵 ⊆ ( Base ‘ 𝑀 )
8 dfss ⊢ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ↔ 𝐵 = ( 𝐵 ∩ ( Base ‘ 𝑀 ) ) )
9 7 8 mpbi ⊢ 𝐵 = ( 𝐵 ∩ ( Base ‘ 𝑀 ) )
10 snex ⊢ { 𝐼 } ∈ V
11 ovex ⊢ ( 0 ..^ 𝑁 ) ∈ V
12 snex ⊢ { ( 𝐺 ‘ 𝑛 ) } ∈ V
13 11 12 iunex ⊢ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ∈ V
14 10 13 unex ⊢ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) ∈ V
15 5 14 eqeltri ⊢ 𝐵 ∈ V
16 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
17 6 16 ressbas ⊢ ( 𝐵 ∈ V → ( 𝐵 ∩ ( Base ‘ 𝑀 ) ) = ( Base ‘ 𝑆 ) )
18 15 17 ax-mp ⊢ ( 𝐵 ∩ ( Base ‘ 𝑀 ) ) = ( Base ‘ 𝑆 )
19 9 18 eqtr2i ⊢ ( Base ‘ 𝑆 ) = 𝐵