Theorem lpssat

Description: Two subspaces in a proper subset relationship imply the existence of an atom less than or equal to one but not the other. ( chpssati analog.) (Contributed by NM, 11-Jan-2015)

	Ref	Expression
Hypotheses	lpssat.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
	lpssat.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
	lpssat.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lpssat.t	$$⊢\phi \to T\in S$$
	lpssat.u	$$⊢\phi \to U\in S$$
	lpssat.l	$$⊢\phi \to T\subset U$$
Assertion	lpssat	$$⊢\phi \to \exists q\in A\left(q\subseteq U\wedge \neg q\subseteq T\right)$$

Proof

Step	Hyp	Ref	Expression
1		lpssat.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
2		lpssat.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
3		lpssat.w	$$⊢\phi \to W\in \mathrm{LMod}$$
4		lpssat.t	$$⊢\phi \to T\in S$$
5		lpssat.u	$$⊢\phi \to U\in S$$
6		lpssat.l	$$⊢\phi \to T\subset U$$
7		dfpss3	$$⊢T\subset U\leftrightarrow \left(T\subseteq U\wedge \neg U\subseteq T\right)$$
8	7	simprbi	$$⊢T\subset U\to \neg U\subseteq T$$
9	6 8	syl	$$⊢\phi \to \neg U\subseteq T$$
10		iman	$$⊢\left(q\subseteq U\to q\subseteq T\right)\leftrightarrow \neg \left(q\subseteq U\wedge \neg q\subseteq T\right)$$
11	10	ralbii	$$⊢\forall q\in A\left(q\subseteq U\to q\subseteq T\right)\leftrightarrow \forall q\in A\neg \left(q\subseteq U\wedge \neg q\subseteq T\right)$$
12		ss2rab	$$⊢\left\{q\in A|q\subseteq U\right\}\subseteq \left\{q\in A|q\subseteq T\right\}\leftrightarrow \forall q\in A\left(q\subseteq U\to q\subseteq T\right)$$
13	3	adantr	$$⊢\left(\phi \wedge \left\{q\in A|q\subseteq U\right\}\subseteq \left\{q\in A|q\subseteq T\right\}\right)\to W\in \mathrm{LMod}$$
14	1 2	lsatlss	$$⊢W\in \mathrm{LMod}\to A\subseteq S$$
15		rabss2	$$⊢A\subseteq S\to \left\{q\in A|q\subseteq T\right\}\subseteq \left\{q\in S|q\subseteq T\right\}$$
16		uniss	$$⊢\left\{q\in A|q\subseteq T\right\}\subseteq \left\{q\in S|q\subseteq T\right\}\to \bigcup \left\{q\in A|q\subseteq T\right\}\subseteq \bigcup \left\{q\in S|q\subseteq T\right\}$$
17	3 14 15 16	4syl	$$⊢\phi \to \bigcup \left\{q\in A|q\subseteq T\right\}\subseteq \bigcup \left\{q\in S|q\subseteq T\right\}$$
18		unimax	$$⊢T\in S\to \bigcup \left\{q\in S|q\subseteq T\right\}=T$$
19	4 18	syl	$$⊢\phi \to \bigcup \left\{q\in S|q\subseteq T\right\}=T$$
20		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
21	20 1	lssss	$$⊢T\in S\to T\subseteq {\mathrm{Base}}_W$$
22	4 21	syl	$$⊢\phi \to T\subseteq {\mathrm{Base}}_W$$
23	19 22	eqsstrd	$$⊢\phi \to \bigcup \left\{q\in S|q\subseteq T\right\}\subseteq {\mathrm{Base}}_W$$
24	17 23	sstrd	$$⊢\phi \to \bigcup \left\{q\in A|q\subseteq T\right\}\subseteq {\mathrm{Base}}_W$$
25	24	adantr	$$⊢\left(\phi \wedge \left\{q\in A|q\subseteq U\right\}\subseteq \left\{q\in A|q\subseteq T\right\}\right)\to \bigcup \left\{q\in A|q\subseteq T\right\}\subseteq {\mathrm{Base}}_W$$
26		uniss	$$⊢\left\{q\in A|q\subseteq U\right\}\subseteq \left\{q\in A|q\subseteq T\right\}\to \bigcup \left\{q\in A|q\subseteq U\right\}\subseteq \bigcup \left\{q\in A|q\subseteq T\right\}$$
27	26	adantl	$$⊢\left(\phi \wedge \left\{q\in A|q\subseteq U\right\}\subseteq \left\{q\in A|q\subseteq T\right\}\right)\to \bigcup \left\{q\in A|q\subseteq U\right\}\subseteq \bigcup \left\{q\in A|q\subseteq T\right\}$$
28		eqid	$$⊢\mathrm{LSpan}\left(W\right)=\mathrm{LSpan}\left(W\right)$$
29	20 28	lspss	$$⊢\left(W\in \mathrm{LMod}\wedge \bigcup \left\{q\in A|q\subseteq T\right\}\subseteq {\mathrm{Base}}_W\wedge \bigcup \left\{q\in A|q\subseteq U\right\}\subseteq \bigcup \left\{q\in A|q\subseteq T\right\}\right)\to \mathrm{LSpan}\left(W\right)\left(\bigcup \left\{q\in A|q\subseteq U\right\}\right)\subseteq \mathrm{LSpan}\left(W\right)\left(\bigcup \left\{q\in A|q\subseteq T\right\}\right)$$
30	13 25 27 29	syl3anc	$$⊢\left(\phi \wedge \left\{q\in A|q\subseteq U\right\}\subseteq \left\{q\in A|q\subseteq T\right\}\right)\to \mathrm{LSpan}\left(W\right)\left(\bigcup \left\{q\in A|q\subseteq U\right\}\right)\subseteq \mathrm{LSpan}\left(W\right)\left(\bigcup \left\{q\in A|q\subseteq T\right\}\right)$$
31	1 28 2	lssats	$$⊢\left(W\in \mathrm{LMod}\wedge U\in S\right)\to U=\mathrm{LSpan}\left(W\right)\left(\bigcup \left\{q\in A|q\subseteq U\right\}\right)$$
32	3 5 31	syl2anc	$$⊢\phi \to U=\mathrm{LSpan}\left(W\right)\left(\bigcup \left\{q\in A|q\subseteq U\right\}\right)$$
33	32	adantr	$$⊢\left(\phi \wedge \left\{q\in A|q\subseteq U\right\}\subseteq \left\{q\in A|q\subseteq T\right\}\right)\to U=\mathrm{LSpan}\left(W\right)\left(\bigcup \left\{q\in A|q\subseteq U\right\}\right)$$
34	1 28 2	lssats	$$⊢\left(W\in \mathrm{LMod}\wedge T\in S\right)\to T=\mathrm{LSpan}\left(W\right)\left(\bigcup \left\{q\in A|q\subseteq T\right\}\right)$$
35	3 4 34	syl2anc	$$⊢\phi \to T=\mathrm{LSpan}\left(W\right)\left(\bigcup \left\{q\in A|q\subseteq T\right\}\right)$$
36	35	adantr	$$⊢\left(\phi \wedge \left\{q\in A|q\subseteq U\right\}\subseteq \left\{q\in A|q\subseteq T\right\}\right)\to T=\mathrm{LSpan}\left(W\right)\left(\bigcup \left\{q\in A|q\subseteq T\right\}\right)$$
37	30 33 36	3sstr4d	$$⊢\left(\phi \wedge \left\{q\in A|q\subseteq U\right\}\subseteq \left\{q\in A|q\subseteq T\right\}\right)\to U\subseteq T$$
38	37	ex	$$⊢\phi \to \left(\left\{q\in A|q\subseteq U\right\}\subseteq \left\{q\in A|q\subseteq T\right\}\to U\subseteq T\right)$$
39	12 38	biimtrrid	$$⊢\phi \to \left(\forall q\in A\left(q\subseteq U\to q\subseteq T\right)\to U\subseteq T\right)$$
40	11 39	biimtrrid	$$⊢\phi \to \left(\forall q\in A\neg \left(q\subseteq U\wedge \neg q\subseteq T\right)\to U\subseteq T\right)$$
41	9 40	mtod	$$⊢\phi \to \neg \forall q\in A\neg \left(q\subseteq U\wedge \neg q\subseteq T\right)$$
42		dfrex2	$$⊢\exists q\in A\left(q\subseteq U\wedge \neg q\subseteq T\right)\leftrightarrow \neg \forall q\in A\neg \left(q\subseteq U\wedge \neg q\subseteq T\right)$$
43	41 42	sylibr	$$⊢\phi \to \exists q\in A\left(q\subseteq U\wedge \neg q\subseteq T\right)$$