Metamath Proof Explorer


Theorem pwslnmlem1

Description: First powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Hypothesis pwslnmlem1.y Y=W𝑠i
Assertion pwslnmlem1 WLNoeMYLNoeM

Proof

Step Hyp Ref Expression
1 pwslnmlem1.y Y=W𝑠i
2 lnmlmod WLNoeMWLMod
3 snex iV
4 eqid BaseW=BaseW
5 eqid xBaseWi×x=xBaseWi×x
6 1 4 5 pwsdiaglmhm WLModiVxBaseWi×xWLMHomY
7 2 3 6 sylancl WLNoeMxBaseWi×xWLMHomY
8 id WLNoeMWLNoeM
9 eqid BaseY=BaseY
10 1 4 5 9 pwssnf1o WLNoeMiVxBaseWi×x:BaseW1-1 ontoBaseY
11 10 elvd WLNoeMxBaseWi×x:BaseW1-1 ontoBaseY
12 f1ofo xBaseWi×x:BaseW1-1 ontoBaseYxBaseWi×x:BaseWontoBaseY
13 forn xBaseWi×x:BaseWontoBaseYranxBaseWi×x=BaseY
14 11 12 13 3syl WLNoeMranxBaseWi×x=BaseY
15 9 lnmepi xBaseWi×xWLMHomYWLNoeMranxBaseWi×x=BaseYYLNoeM
16 7 8 14 15 syl3anc WLNoeMYLNoeM