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