Theorem pwslnmlem0

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

	Ref	Expression
Hypothesis	pwslnmlem0.y	$$⊢Y=W{\uparrow }_{𝑠}\varnothing$$
Assertion	pwslnmlem0	$$⊢W\in \mathrm{LMod}\to Y\in \mathrm{LNoeM}$$

Proof

Step	Hyp	Ref	Expression
1		pwslnmlem0.y	$$⊢Y=W{\uparrow }_{𝑠}\varnothing$$
2		0ex	$$⊢\varnothing \in \mathrm{V}$$
3	1	pwslmod	$$⊢\left(W\in \mathrm{LMod}\wedge \varnothing \in \mathrm{V}\right)\to Y\in \mathrm{LMod}$$
4	2 3	mpan2	$$⊢W\in \mathrm{LMod}\to Y\in \mathrm{LMod}$$
5		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
6	1 5	pwsbas	$$⊢\left(W\in \mathrm{LMod}\wedge \varnothing \in \mathrm{V}\right)\to {{\mathrm{Base}}_W}^{\varnothing }={\mathrm{Base}}_Y$$
7	2 6	mpan2	$$⊢W\in \mathrm{LMod}\to {{\mathrm{Base}}_W}^{\varnothing }={\mathrm{Base}}_Y$$
8		fvex	$$⊢{\mathrm{Base}}_W\in \mathrm{V}$$
9		map0e	$$⊢{\mathrm{Base}}_W\in \mathrm{V}\to {{\mathrm{Base}}_W}^{\varnothing }=1_{𝑜}$$
10	8 9	ax-mp	$$⊢{{\mathrm{Base}}_W}^{\varnothing }=1_{𝑜}$$
11		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
12	10 11	eqtri	$$⊢{{\mathrm{Base}}_W}^{\varnothing }=\left\{\varnothing \right\}$$
13		snfi	$$⊢\left\{\varnothing \right\}\in \mathrm{Fin}$$
14	12 13	eqeltri	$$⊢{{\mathrm{Base}}_W}^{\varnothing }\in \mathrm{Fin}$$
15	7 14	eqeltrrdi	$$⊢W\in \mathrm{LMod}\to {\mathrm{Base}}_Y\in \mathrm{Fin}$$
16		eqid	$$⊢{\mathrm{Base}}_Y={\mathrm{Base}}_Y$$
17	16	filnm	$$⊢\left(Y\in \mathrm{LMod}\wedge {\mathrm{Base}}_Y\in \mathrm{Fin}\right)\to Y\in \mathrm{LNoeM}$$
18	4 15 17	syl2anc	$$⊢W\in \mathrm{LMod}\to Y\in \mathrm{LNoeM}$$