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 No typesetting found for |- M = ( EndoFMnd ` NN0 ) with typecode |-
smndex1ibas.n N
smndex1ibas.i I=x0xmodN
smndex1ibas.g G=n0..^Nx0n
smndex1mgm.b B=In0..^NGn
smndex1mgm.s S=M𝑠B
Assertion smndex1n0mnd 0MB

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=x0xmodN
4 smndex1ibas.g G=n0..^Nx0n
5 smndex1mgm.b B=In0..^NGn
6 smndex1mgm.s S=M𝑠B
7 nnnn0 NN0
8 fveq2 x=NI0x=I0N
9 2 7 ax-mp N0
10 fvresi N0I0N=N
11 9 10 ax-mp I0N=N
12 8 11 eqtrdi x=NI0x=N
13 fveq2 x=NIx=IN
14 12 13 eqeq12d x=NI0x=IxN=IN
15 14 notbid x=N¬I0x=Ix¬N=IN
16 15 adantl Nx=N¬I0x=Ix¬N=IN
17 nnne0 NN0
18 17 neneqd N¬N=0
19 oveq1 x=NxmodN=NmodN
20 nnrp NN+
21 modid0 N+NmodN=0
22 20 21 syl NNmodN=0
23 19 22 sylan9eqr Nx=NxmodN=0
24 c0ex 0V
25 24 a1i N0V
26 3 23 7 25 fvmptd2 NIN=0
27 26 eqeq2d NN=INN=0
28 18 27 mtbird N¬N=IN
29 7 16 28 rspcedvd Nx0¬I0x=Ix
30 2 29 ax-mp x0¬I0x=Ix
31 rexnal x0¬I0x=Ix¬x0I0x=Ix
32 30 31 mpbi ¬x0I0x=Ix
33 fnresi I0Fn0
34 ovex xmodNV
35 34 3 fnmpti IFn0
36 eqfnfv I0Fn0IFn0I0=Ix0I0x=Ix
37 33 35 36 mp2an I0=Ix0I0x=Ix
38 32 37 mtbir ¬I0=I
39 9 a1i n0..^NN0
40 fveq2 x=NGnx=GnN
41 12 40 eqeq12d x=NI0x=GnxN=GnN
42 41 notbid x=N¬I0x=Gnx¬N=GnN
43 42 adantl n0..^Nx=N¬I0x=Gnx¬N=GnN
44 fzonel ¬N0..^N
45 eleq1 n=Nn0..^NN0..^N
46 45 eqcoms N=nn0..^NN0..^N
47 44 46 mtbiri N=n¬n0..^N
48 47 con2i n0..^N¬N=n
49 nn0ex 0V
50 49 mptex x0nV
51 4 fvmpt2 n0..^Nx0nVGn=x0n
52 50 51 mpan2 n0..^NGn=x0n
53 eqidd n0..^Nx=Nn=n
54 id n0..^Nn0..^N
55 52 53 39 54 fvmptd n0..^NGnN=n
56 55 eqeq2d n0..^NN=GnNN=n
57 48 56 mtbird n0..^N¬N=GnN
58 39 43 57 rspcedvd n0..^Nx0¬I0x=Gnx
59 rexnal x0¬I0x=Gnx¬x0I0x=Gnx
60 58 59 sylib n0..^N¬x0I0x=Gnx
61 vex nV
62 eqid x0n=x0n
63 61 62 fnmpti x0nFn0
64 52 fneq1d n0..^NGnFn0x0nFn0
65 63 64 mpbiri n0..^NGnFn0
66 eqfnfv I0Fn0GnFn0I0=Gnx0I0x=Gnx
67 33 65 66 sylancr n0..^NI0=Gnx0I0x=Gnx
68 60 67 mtbird n0..^N¬I0=Gn
69 68 nrex ¬n0..^NI0=Gn
70 38 69 pm3.2ni ¬I0=In0..^NI0=Gn
71 1 efmndid 0VI0=0M
72 49 71 ax-mp I0=0M
73 72 eqcomi 0M=I0
74 73 5 eleq12i 0MBI0In0..^NGn
75 elun I0In0..^NGnI0II0n0..^NGn
76 resiexg 0VI0V
77 49 76 ax-mp I0V
78 77 elsn I0II0=I
79 eliun I0n0..^NGnn0..^NI0Gn
80 77 elsn I0GnI0=Gn
81 80 rexbii n0..^NI0Gnn0..^NI0=Gn
82 79 81 bitri I0n0..^NGnn0..^NI0=Gn
83 78 82 orbi12i I0II0n0..^NGnI0=In0..^NI0=Gn
84 75 83 bitri I0In0..^NGnI0=In0..^NI0=Gn
85 74 84 bitri 0MBI0=In0..^NI0=Gn
86 70 85 mtbir ¬0MB
87 86 nelir 0MB