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

Metamath Proof Explorer

Theorem smndex1basss

Description: The modulo function I and the constant functions ( GK ) are endofunctions on NN0 . (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 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } )
Assertion smndex1basss 𝐵 ⊆ ( 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 5 eleq2i ⊢ ( 𝑏 ∈ 𝐵 ↔ 𝑏 ∈ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) )
7 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑘 ) )
8 7 sneqd ⊢ ( 𝑛 = 𝑘 → { ( 𝐺 ‘ 𝑛 ) } = { ( 𝐺 ‘ 𝑘 ) } )
9 8 cbviunv ⊢ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } = ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) }
10 9 uneq2i ⊢ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) = ( { 𝐼 } ∪ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } )
11 10 eleq2i ⊢ ( 𝑏 ∈ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) ↔ 𝑏 ∈ ( { 𝐼 } ∪ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ) )
12 6 11 bitri ⊢ ( 𝑏 ∈ 𝐵 ↔ 𝑏 ∈ ( { 𝐼 } ∪ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ) )
13 elun ⊢ ( 𝑏 ∈ ( { 𝐼 } ∪ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ) ↔ ( 𝑏 ∈ { 𝐼 } ∨ 𝑏 ∈ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ) )
14 velsn ⊢ ( 𝑏 ∈ { 𝐼 } ↔ 𝑏 = 𝐼 )
15 eliun ⊢ ( 𝑏 ∈ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ↔ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑏 ∈ { ( 𝐺 ‘ 𝑘 ) } )
16 14 15 orbi12i ⊢ ( ( 𝑏 ∈ { 𝐼 } ∨ 𝑏 ∈ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ) ↔ ( 𝑏 = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑏 ∈ { ( 𝐺 ‘ 𝑘 ) } ) )
17 12 13 16 3bitri ⊢ ( 𝑏 ∈ 𝐵 ↔ ( 𝑏 = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑏 ∈ { ( 𝐺 ‘ 𝑘 ) } ) )
18 1 2 3 smndex1ibas ⊢ 𝐼 ∈ ( Base ‘ 𝑀 )
19 eleq1 ⊢ ( 𝑏 = 𝐼 → ( 𝑏 ∈ ( Base ‘ 𝑀 ) ↔ 𝐼 ∈ ( Base ‘ 𝑀 ) ) )
20 18 19 mpbiri ⊢ ( 𝑏 = 𝐼 → 𝑏 ∈ ( Base ‘ 𝑀 ) )
21 1 2 3 4 smndex1gbas ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝑘 ) ∈ ( Base ‘ 𝑀 ) )
22 21 adantr ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑏 ∈ { ( 𝐺 ‘ 𝑘 ) } ) → ( 𝐺 ‘ 𝑘 ) ∈ ( Base ‘ 𝑀 ) )
23 elsni ⊢ ( 𝑏 ∈ { ( 𝐺 ‘ 𝑘 ) } → 𝑏 = ( 𝐺 ‘ 𝑘 ) )
24 23 eleq1d ⊢ ( 𝑏 ∈ { ( 𝐺 ‘ 𝑘 ) } → ( 𝑏 ∈ ( Base ‘ 𝑀 ) ↔ ( 𝐺 ‘ 𝑘 ) ∈ ( Base ‘ 𝑀 ) ) )
25 24 adantl ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑏 ∈ { ( 𝐺 ‘ 𝑘 ) } ) → ( 𝑏 ∈ ( Base ‘ 𝑀 ) ↔ ( 𝐺 ‘ 𝑘 ) ∈ ( Base ‘ 𝑀 ) ) )
26 22 25 mpbird ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑏 ∈ { ( 𝐺 ‘ 𝑘 ) } ) → 𝑏 ∈ ( Base ‘ 𝑀 ) )
27 26 rexlimiva ⊢ ( ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑏 ∈ { ( 𝐺 ‘ 𝑘 ) } → 𝑏 ∈ ( Base ‘ 𝑀 ) )
28 20 27 jaoi ⊢ ( ( 𝑏 = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑏 ∈ { ( 𝐺 ‘ 𝑘 ) } ) → 𝑏 ∈ ( Base ‘ 𝑀 ) )
29 17 28 sylbi ⊢ ( 𝑏 ∈ 𝐵 → 𝑏 ∈ ( Base ‘ 𝑀 ) )
30 29 ssriv ⊢ 𝐵 ⊆ ( Base ‘ 𝑀 )