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 
|- M = ( EndoFMnd ` NN0 )
smndex1ibas.n 
|- N e. NN
smndex1ibas.i 
|- I = ( x e. NN0 |-> ( x mod N ) )
smndex1ibas.g 
|- G = ( n e. ( 0 ..^ N ) |-> ( x e. NN0 |-> n ) )
smndex1mgm.b 
|- B = ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } )
Assertion smndex1basss 
|- B C_ ( Base ` M )

Proof

Step Hyp Ref Expression
1 smndex1ibas.m 
 |-  M = ( EndoFMnd ` NN0 )
2 smndex1ibas.n 
 |-  N e. NN
3 smndex1ibas.i 
 |-  I = ( x e. NN0 |-> ( x mod N ) )
4 smndex1ibas.g 
 |-  G = ( n e. ( 0 ..^ N ) |-> ( x e. NN0 |-> n ) )
5 smndex1mgm.b 
 |-  B = ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } )
6 5 eleq2i 
 |-  ( b e. B <-> b e. ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) )
7 fveq2 
 |-  ( n = k -> ( G ` n ) = ( G ` k ) )
8 7 sneqd 
 |-  ( n = k -> { ( G ` n ) } = { ( G ` k ) } )
9 8 cbviunv 
 |-  U_ n e. ( 0 ..^ N ) { ( G ` n ) } = U_ k e. ( 0 ..^ N ) { ( G ` k ) }
10 9 uneq2i 
 |-  ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) = ( { I } u. U_ k e. ( 0 ..^ N ) { ( G ` k ) } )
11 10 eleq2i 
 |-  ( b e. ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) <-> b e. ( { I } u. U_ k e. ( 0 ..^ N ) { ( G ` k ) } ) )
12 6 11 bitri 
 |-  ( b e. B <-> b e. ( { I } u. U_ k e. ( 0 ..^ N ) { ( G ` k ) } ) )
13 elun 
 |-  ( b e. ( { I } u. U_ k e. ( 0 ..^ N ) { ( G ` k ) } ) <-> ( b e. { I } \/ b e. U_ k e. ( 0 ..^ N ) { ( G ` k ) } ) )
14 velsn 
 |-  ( b e. { I } <-> b = I )
15 eliun 
 |-  ( b e. U_ k e. ( 0 ..^ N ) { ( G ` k ) } <-> E. k e. ( 0 ..^ N ) b e. { ( G ` k ) } )
16 14 15 orbi12i 
 |-  ( ( b e. { I } \/ b e. U_ k e. ( 0 ..^ N ) { ( G ` k ) } ) <-> ( b = I \/ E. k e. ( 0 ..^ N ) b e. { ( G ` k ) } ) )
17 12 13 16 3bitri 
 |-  ( b e. B <-> ( b = I \/ E. k e. ( 0 ..^ N ) b e. { ( G ` k ) } ) )
18 1 2 3 smndex1ibas 
 |-  I e. ( Base ` M )
19 eleq1 
 |-  ( b = I -> ( b e. ( Base ` M ) <-> I e. ( Base ` M ) ) )
20 18 19 mpbiri 
 |-  ( b = I -> b e. ( Base ` M ) )
21 1 2 3 4 smndex1gbas 
 |-  ( k e. ( 0 ..^ N ) -> ( G ` k ) e. ( Base ` M ) )
22 21 adantr 
 |-  ( ( k e. ( 0 ..^ N ) /\ b e. { ( G ` k ) } ) -> ( G ` k ) e. ( Base ` M ) )
23 elsni 
 |-  ( b e. { ( G ` k ) } -> b = ( G ` k ) )
24 23 eleq1d 
 |-  ( b e. { ( G ` k ) } -> ( b e. ( Base ` M ) <-> ( G ` k ) e. ( Base ` M ) ) )
25 24 adantl 
 |-  ( ( k e. ( 0 ..^ N ) /\ b e. { ( G ` k ) } ) -> ( b e. ( Base ` M ) <-> ( G ` k ) e. ( Base ` M ) ) )
26 22 25 mpbird 
 |-  ( ( k e. ( 0 ..^ N ) /\ b e. { ( G ` k ) } ) -> b e. ( Base ` M ) )
27 26 rexlimiva 
 |-  ( E. k e. ( 0 ..^ N ) b e. { ( G ` k ) } -> b e. ( Base ` M ) )
28 20 27 jaoi 
 |-  ( ( b = I \/ E. k e. ( 0 ..^ N ) b e. { ( G ` k ) } ) -> b e. ( Base ` M ) )
29 17 28 sylbi 
 |-  ( b e. B -> b e. ( Base ` M ) )
30 29 ssriv 
 |-  B C_ ( Base ` M )