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