Description: First powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | pwslnmlem1.y | |
|
Assertion | pwslnmlem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pwslnmlem1.y | |
|
2 | lnmlmod | |
|
3 | snex | |
|
4 | eqid | |
|
5 | eqid | |
|
6 | 1 4 5 | pwsdiaglmhm | |
7 | 2 3 6 | sylancl | |
8 | id | |
|
9 | eqid | |
|
10 | 1 4 5 9 | pwssnf1o | |
11 | 10 | elvd | |
12 | f1ofo | |
|
13 | forn | |
|
14 | 11 12 13 | 3syl | |
15 | 9 | lnmepi | |
16 | 7 8 14 15 | syl3anc | |