Metamath Proof Explorer

Theorem smndex1n0mnd

Description: The identity of the monoid M of endofunctions on set NN0 is not contained in the base set of the constructed monoid S . (Contributed by AV, 17-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 ) } )
smndex1mgm.s 
|- S = ( M |`s B )
Assertion smndex1n0mnd 
|- ( 0g ` M ) e/ B

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 smndex1mgm.s 
 |-  S = ( M |`s B )
7 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
8 fveq2 
 |-  ( x = N -> ( ( _I |` NN0 ) ` x ) = ( ( _I |` NN0 ) ` N ) )
9 2 7 ax-mp 
 |-  N e. NN0
10 fvresi 
 |-  ( N e. NN0 -> ( ( _I |` NN0 ) ` N ) = N )
11 9 10 ax-mp 
 |-  ( ( _I |` NN0 ) ` N ) = N
12 8 11 syl6eq 
 |-  ( x = N -> ( ( _I |` NN0 ) ` x ) = N )
13 fveq2 
 |-  ( x = N -> ( I ` x ) = ( I ` N ) )
14 12 13 eqeq12d 
 |-  ( x = N -> ( ( ( _I |` NN0 ) ` x ) = ( I ` x ) <-> N = ( I ` N ) ) )
15 14 notbid 
 |-  ( x = N -> ( -. ( ( _I |` NN0 ) ` x ) = ( I ` x ) <-> -. N = ( I ` N ) ) )
16 15 adantl 
 |-  ( ( N e. NN /\ x = N ) -> ( -. ( ( _I |` NN0 ) ` x ) = ( I ` x ) <-> -. N = ( I ` N ) ) )
17 nnne0 
 |-  ( N e. NN -> N =/= 0 )
18 17 neneqd 
 |-  ( N e. NN -> -. N = 0 )
19 oveq1 
 |-  ( x = N -> ( x mod N ) = ( N mod N ) )
20 nnrp 
 |-  ( N e. NN -> N e. RR+ )
21 modid0 
 |-  ( N e. RR+ -> ( N mod N ) = 0 )
22 20 21 syl 
 |-  ( N e. NN -> ( N mod N ) = 0 )
23 19 22 sylan9eqr 
 |-  ( ( N e. NN /\ x = N ) -> ( x mod N ) = 0 )
24 c0ex 
 |-  0 e. _V
25 24 a1i 
 |-  ( N e. NN -> 0 e. _V )
26 3 23 7 25 fvmptd2 
 |-  ( N e. NN -> ( I ` N ) = 0 )
27 26 eqeq2d 
 |-  ( N e. NN -> ( N = ( I ` N ) <-> N = 0 ) )
28 18 27 mtbird 
 |-  ( N e. NN -> -. N = ( I ` N ) )
29 7 16 28 rspcedvd 
 |-  ( N e. NN -> E. x e. NN0 -. ( ( _I |` NN0 ) ` x ) = ( I ` x ) )
30 2 29 ax-mp 
 |-  E. x e. NN0 -. ( ( _I |` NN0 ) ` x ) = ( I ` x )
31 rexnal 
 |-  ( E. x e. NN0 -. ( ( _I |` NN0 ) ` x ) = ( I ` x ) <-> -. A. x e. NN0 ( ( _I |` NN0 ) ` x ) = ( I ` x ) )
32 30 31 mpbi 
 |-  -. A. x e. NN0 ( ( _I |` NN0 ) ` x ) = ( I ` x )
33 fnresi 
 |-  ( _I |` NN0 ) Fn NN0
34 ovex 
 |-  ( x mod N ) e. _V
35 34 3 fnmpti 
 |-  I Fn NN0
36 eqfnfv 
 |-  ( ( ( _I |` NN0 ) Fn NN0 /\ I Fn NN0 ) -> ( ( _I |` NN0 ) = I <-> A. x e. NN0 ( ( _I |` NN0 ) ` x ) = ( I ` x ) ) )
37 33 35 36 mp2an 
 |-  ( ( _I |` NN0 ) = I <-> A. x e. NN0 ( ( _I |` NN0 ) ` x ) = ( I ` x ) )
38 32 37 mtbir 
 |-  -. ( _I |` NN0 ) = I
39 9 a1i 
 |-  ( n e. ( 0 ..^ N ) -> N e. NN0 )
40 fveq2 
 |-  ( x = N -> ( ( G ` n ) ` x ) = ( ( G ` n ) ` N ) )
41 12 40 eqeq12d 
 |-  ( x = N -> ( ( ( _I |` NN0 ) ` x ) = ( ( G ` n ) ` x ) <-> N = ( ( G ` n ) ` N ) ) )
42 41 notbid 
 |-  ( x = N -> ( -. ( ( _I |` NN0 ) ` x ) = ( ( G ` n ) ` x ) <-> -. N = ( ( G ` n ) ` N ) ) )
43 42 adantl 
 |-  ( ( n e. ( 0 ..^ N ) /\ x = N ) -> ( -. ( ( _I |` NN0 ) ` x ) = ( ( G ` n ) ` x ) <-> -. N = ( ( G ` n ) ` N ) ) )
44 fzonel 
 |-  -. N e. ( 0 ..^ N )
45 eleq1 
 |-  ( n = N -> ( n e. ( 0 ..^ N ) <-> N e. ( 0 ..^ N ) ) )
46 45 eqcoms 
 |-  ( N = n -> ( n e. ( 0 ..^ N ) <-> N e. ( 0 ..^ N ) ) )
47 44 46 mtbiri 
 |-  ( N = n -> -. n e. ( 0 ..^ N ) )
48 47 con2i 
 |-  ( n e. ( 0 ..^ N ) -> -. N = n )
49 nn0ex 
 |-  NN0 e. _V
50 49 mptex 
 |-  ( x e. NN0 |-> n ) e. _V
51 4 fvmpt2 
 |-  ( ( n e. ( 0 ..^ N ) /\ ( x e. NN0 |-> n ) e. _V ) -> ( G ` n ) = ( x e. NN0 |-> n ) )
52 50 51 mpan2 
 |-  ( n e. ( 0 ..^ N ) -> ( G ` n ) = ( x e. NN0 |-> n ) )
53 eqidd 
 |-  ( ( n e. ( 0 ..^ N ) /\ x = N ) -> n = n )
54 id 
 |-  ( n e. ( 0 ..^ N ) -> n e. ( 0 ..^ N ) )
55 52 53 39 54 fvmptd 
 |-  ( n e. ( 0 ..^ N ) -> ( ( G ` n ) ` N ) = n )
56 55 eqeq2d 
 |-  ( n e. ( 0 ..^ N ) -> ( N = ( ( G ` n ) ` N ) <-> N = n ) )
57 48 56 mtbird 
 |-  ( n e. ( 0 ..^ N ) -> -. N = ( ( G ` n ) ` N ) )
58 39 43 57 rspcedvd 
 |-  ( n e. ( 0 ..^ N ) -> E. x e. NN0 -. ( ( _I |` NN0 ) ` x ) = ( ( G ` n ) ` x ) )
59 rexnal 
 |-  ( E. x e. NN0 -. ( ( _I |` NN0 ) ` x ) = ( ( G ` n ) ` x ) <-> -. A. x e. NN0 ( ( _I |` NN0 ) ` x ) = ( ( G ` n ) ` x ) )
60 58 59 sylib 
 |-  ( n e. ( 0 ..^ N ) -> -. A. x e. NN0 ( ( _I |` NN0 ) ` x ) = ( ( G ` n ) ` x ) )
61 vex 
 |-  n e. _V
62 eqid 
 |-  ( x e. NN0 |-> n ) = ( x e. NN0 |-> n )
63 61 62 fnmpti 
 |-  ( x e. NN0 |-> n ) Fn NN0
64 52 fneq1d 
 |-  ( n e. ( 0 ..^ N ) -> ( ( G ` n ) Fn NN0 <-> ( x e. NN0 |-> n ) Fn NN0 ) )
65 63 64 mpbiri 
 |-  ( n e. ( 0 ..^ N ) -> ( G ` n ) Fn NN0 )
66 eqfnfv 
 |-  ( ( ( _I |` NN0 ) Fn NN0 /\ ( G ` n ) Fn NN0 ) -> ( ( _I |` NN0 ) = ( G ` n ) <-> A. x e. NN0 ( ( _I |` NN0 ) ` x ) = ( ( G ` n ) ` x ) ) )
67 33 65 66 sylancr 
 |-  ( n e. ( 0 ..^ N ) -> ( ( _I |` NN0 ) = ( G ` n ) <-> A. x e. NN0 ( ( _I |` NN0 ) ` x ) = ( ( G ` n ) ` x ) ) )
68 60 67 mtbird 
 |-  ( n e. ( 0 ..^ N ) -> -. ( _I |` NN0 ) = ( G ` n ) )
69 68 nrex 
 |-  -. E. n e. ( 0 ..^ N ) ( _I |` NN0 ) = ( G ` n )
70 38 69 pm3.2ni 
 |-  -. ( ( _I |` NN0 ) = I \/ E. n e. ( 0 ..^ N ) ( _I |` NN0 ) = ( G ` n ) )
71 1 efmndid 
 |-  ( NN0 e. _V -> ( _I |` NN0 ) = ( 0g ` M ) )
72 49 71 ax-mp 
 |-  ( _I |` NN0 ) = ( 0g ` M )
73 72 eqcomi 
 |-  ( 0g ` M ) = ( _I |` NN0 )
74 73 5 eleq12i 
 |-  ( ( 0g ` M ) e. B <-> ( _I |` NN0 ) e. ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) )
75 elun 
 |-  ( ( _I |` NN0 ) e. ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) <-> ( ( _I |` NN0 ) e. { I } \/ ( _I |` NN0 ) e. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) )
76 resiexg 
 |-  ( NN0 e. _V -> ( _I |` NN0 ) e. _V )
77 49 76 ax-mp 
 |-  ( _I |` NN0 ) e. _V
78 77 elsn 
 |-  ( ( _I |` NN0 ) e. { I } <-> ( _I |` NN0 ) = I )
79 eliun 
 |-  ( ( _I |` NN0 ) e. U_ n e. ( 0 ..^ N ) { ( G ` n ) } <-> E. n e. ( 0 ..^ N ) ( _I |` NN0 ) e. { ( G ` n ) } )
80 77 elsn 
 |-  ( ( _I |` NN0 ) e. { ( G ` n ) } <-> ( _I |` NN0 ) = ( G ` n ) )
81 80 rexbii 
 |-  ( E. n e. ( 0 ..^ N ) ( _I |` NN0 ) e. { ( G ` n ) } <-> E. n e. ( 0 ..^ N ) ( _I |` NN0 ) = ( G ` n ) )
82 79 81 bitri 
 |-  ( ( _I |` NN0 ) e. U_ n e. ( 0 ..^ N ) { ( G ` n ) } <-> E. n e. ( 0 ..^ N ) ( _I |` NN0 ) = ( G ` n ) )
83 78 82 orbi12i 
 |-  ( ( ( _I |` NN0 ) e. { I } \/ ( _I |` NN0 ) e. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) <-> ( ( _I |` NN0 ) = I \/ E. n e. ( 0 ..^ N ) ( _I |` NN0 ) = ( G ` n ) ) )
84 75 83 bitri 
 |-  ( ( _I |` NN0 ) e. ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) <-> ( ( _I |` NN0 ) = I \/ E. n e. ( 0 ..^ N ) ( _I |` NN0 ) = ( G ` n ) ) )
85 74 84 bitri 
 |-  ( ( 0g ` M ) e. B <-> ( ( _I |` NN0 ) = I \/ E. n e. ( 0 ..^ N ) ( _I |` NN0 ) = ( G ` n ) ) )
86 70 85 mtbir 
 |-  -. ( 0g ` M ) e. B
87 86 nelir 
 |-  ( 0g ` M ) e/ B