Theorem pwslnmlem0

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

	Ref	Expression
Hypothesis	pwslnmlem0.y	⊢ 𝑌 = ( 𝑊 ↑s ∅ )
Assertion	pwslnmlem0	⊢ ( 𝑊 ∈ LMod → 𝑌 ∈ LNoeM )

Proof

Step	Hyp	Ref	Expression
1		pwslnmlem0.y	⊢ 𝑌 = ( 𝑊 ↑s ∅ )
2		0ex	⊢ ∅ ∈ V
3	1	pwslmod	⊢ ( ( 𝑊 ∈ LMod ∧ ∅ ∈ V ) → 𝑌 ∈ LMod )
4	2 3	mpan2	⊢ ( 𝑊 ∈ LMod → 𝑌 ∈ LMod )
5		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
6	1 5	pwsbas	⊢ ( ( 𝑊 ∈ LMod ∧ ∅ ∈ V ) → ( ( Base ‘ 𝑊 ) ↑m ∅ ) = ( Base ‘ 𝑌 ) )
7	2 6	mpan2	⊢ ( 𝑊 ∈ LMod → ( ( Base ‘ 𝑊 ) ↑m ∅ ) = ( Base ‘ 𝑌 ) )
8		fvex	⊢ ( Base ‘ 𝑊 ) ∈ V
9		map0e	⊢ ( ( Base ‘ 𝑊 ) ∈ V → ( ( Base ‘ 𝑊 ) ↑m ∅ ) = 1o )
10	8 9	ax-mp	⊢ ( ( Base ‘ 𝑊 ) ↑m ∅ ) = 1o
11		df1o2	⊢ 1o = { ∅ }
12	10 11	eqtri	⊢ ( ( Base ‘ 𝑊 ) ↑m ∅ ) = { ∅ }
13		snfi	⊢ { ∅ } ∈ Fin
14	12 13	eqeltri	⊢ ( ( Base ‘ 𝑊 ) ↑m ∅ ) ∈ Fin
15	7 14	eqeltrrdi	⊢ ( 𝑊 ∈ LMod → ( Base ‘ 𝑌 ) ∈ Fin )
16		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
17	16	filnm	⊢ ( ( 𝑌 ∈ LMod ∧ ( Base ‘ 𝑌 ) ∈ Fin ) → 𝑌 ∈ LNoeM )
18	4 15 17	syl2anc	⊢ ( 𝑊 ∈ LMod → 𝑌 ∈ LNoeM )