Theorem lsatssn0

Description: A subspace (or any class) including an atom is nonzero. (Contributed by NM, 3-Feb-2015)

	Ref	Expression
Hypotheses	lsatssn0.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lsatssn0.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
	lsatssn0.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lsatssn0.q	$$⊢\phi \to Q\in A$$
	lsatssn0.u	$$⊢\phi \to Q\subseteq U$$
Assertion	lsatssn0	$$⊢\phi \to U\ne \left\{\underset{\dot{}}{0}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		lsatssn0.o	$$⊢\underset{\dot{}}{0}=0_W$$
2		lsatssn0.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
3		lsatssn0.w	$$⊢\phi \to W\in \mathrm{LMod}$$
4		lsatssn0.q	$$⊢\phi \to Q\in A$$
5		lsatssn0.u	$$⊢\phi \to Q\subseteq U$$
6		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
7	6 2 3 4	lsatlssel	$$⊢\phi \to Q\in \mathrm{LSubSp}\left(W\right)$$
8	1 6	lss0ss	$$⊢\left(W\in \mathrm{LMod}\wedge Q\in \mathrm{LSubSp}\left(W\right)\right)\to \left\{\underset{\dot{}}{0}\right\}\subseteq Q$$
9	3 7 8	syl2anc	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}\subseteq Q$$
10	1 2 3 4	lsatn0	$$⊢\phi \to Q\ne \left\{\underset{\dot{}}{0}\right\}$$
11	10	necomd	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}\ne Q$$
12		df-pss	$$⊢\left\{\underset{\dot{}}{0}\right\}\subset Q\leftrightarrow \left(\left\{\underset{\dot{}}{0}\right\}\subseteq Q\wedge \left\{\underset{\dot{}}{0}\right\}\ne Q\right)$$
13	9 11 12	sylanbrc	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}\subset Q$$
14	13 5	psssstrd	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}\subset U$$
15	14	pssned	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}\ne U$$
16	15	necomd	$$⊢\phi \to U\ne \left\{\underset{\dot{}}{0}\right\}$$