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 No typesetting found for |- M = ( EndoFMnd ` NN0 ) with typecode |-
smndex1ibas.n ⊢N∈ℕ
smndex1ibas.i ⊢I=x∈ℕ0⟼xmodN
smndex1ibas.g ⊢G=n∈0..^N⟼x∈ℕ0⟼n
smndex1mgm.b ⊢B=I∪⋃n∈0..^NG⁡n
Assertion smndex1basss ⊢B⊆BaseM

Proof

Step Hyp Ref Expression
1 smndex1ibas.m Could not format M = ( EndoFMnd ` NN0 ) : No typesetting found for |- M = ( EndoFMnd ` NN0 ) with typecode |-
2 smndex1ibas.n ⊢N∈ℕ
3 smndex1ibas.i ⊢I=x∈ℕ0⟼xmodN
4 smndex1ibas.g ⊢G=n∈0..^N⟼x∈ℕ0⟼n
5 smndex1mgm.b ⊢B=I∪⋃n∈0..^NG⁡n
6 5 eleq2i ⊢b∈B↔b∈I∪⋃n∈0..^NG⁡n
7 fveq2 ⊢n=k→G⁡n=G⁡k
8 7 sneqd ⊢n=k→G⁡n=G⁡k
9 8 cbviunv ⊢⋃n∈0..^NG⁡n=⋃k∈0..^NG⁡k
10 9 uneq2i ⊢I∪⋃n∈0..^NG⁡n=I∪⋃k∈0..^NG⁡k
11 10 eleq2i ⊢b∈I∪⋃n∈0..^NG⁡n↔b∈I∪⋃k∈0..^NG⁡k
12 6 11 bitri ⊢b∈B↔b∈I∪⋃k∈0..^NG⁡k
13 elun ⊢b∈I∪⋃k∈0..^NG⁡k↔b∈I∨b∈⋃k∈0..^NG⁡k
14 velsn ⊢b∈I↔b=I
15 eliun ⊢b∈⋃k∈0..^NG⁡k↔∃k∈0..^Nb∈G⁡k
16 14 15 orbi12i ⊢b∈I∨b∈⋃k∈0..^NG⁡k↔b=I∨∃k∈0..^Nb∈G⁡k
17 12 13 16 3bitri ⊢b∈B↔b=I∨∃k∈0..^Nb∈G⁡k
18 1 2 3 smndex1ibas ⊢I∈BaseM
19 eleq1 ⊢b=I→b∈BaseM↔I∈BaseM
20 18 19 mpbiri ⊢b=I→b∈BaseM
21 1 2 3 4 smndex1gbas ⊢k∈0..^N→G⁡k∈BaseM
22 21 adantr ⊢k∈0..^N∧b∈G⁡k→G⁡k∈BaseM
23 elsni ⊢b∈G⁡k→b=G⁡k
24 23 eleq1d ⊢b∈G⁡k→b∈BaseM↔G⁡k∈BaseM
25 24 adantl ⊢k∈0..^N∧b∈G⁡k→b∈BaseM↔G⁡k∈BaseM
26 22 25 mpbird ⊢k∈0..^N∧b∈G⁡k→b∈BaseM
27 26 rexlimiva ⊢∃k∈0..^Nb∈G⁡k→b∈BaseM
28 20 27 jaoi ⊢b=I∨∃k∈0..^Nb∈G⁡k→b∈BaseM
29 17 28 sylbi ⊢b∈B→b∈BaseM
30 29 ssriv ⊢B⊆BaseM