Theorem lsatcmp2

Description: If an atom is included in at-most an atom, they are equal. More general version of lsatcmp . TODO: can lspsncmp shorten this? (Contributed by NM, 3-Feb-2015)

	Ref	Expression
Hypotheses	lsatcmp2.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lsatcmp2.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
	lsatcmp2.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lsatcmp2.t	$$⊢\phi \to T\in A$$
	lsatcmp2.u	$$⊢\phi \to \left(U\in A\vee U=\left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	lsatcmp2	$$⊢\phi \to \left(T\subseteq U\leftrightarrow T=U\right)$$

Proof

Step	Hyp	Ref	Expression
1		lsatcmp2.o	$$⊢\underset{\dot{}}{0}=0_W$$
2		lsatcmp2.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
3		lsatcmp2.w	$$⊢\phi \to W\in \mathrm{LVec}$$
4		lsatcmp2.t	$$⊢\phi \to T\in A$$
5		lsatcmp2.u	$$⊢\phi \to \left(U\in A\vee U=\left\{\underset{\dot{}}{0}\right\}\right)$$
6		simpr	$$⊢\left(\phi \wedge T\subseteq U\right)\to T\subseteq U$$
7	3	adantr	$$⊢\left(\phi \wedge T\subseteq U\right)\to W\in \mathrm{LVec}$$
8	4	adantr	$$⊢\left(\phi \wedge T\subseteq U\right)\to T\in A$$
9		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
10	3 9	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
11	10	adantr	$$⊢\left(\phi \wedge T\subseteq U\right)\to W\in \mathrm{LMod}$$
12	1 2 11 8 6	lsatssn0	$$⊢\left(\phi \wedge T\subseteq U\right)\to U\ne \left\{\underset{\dot{}}{0}\right\}$$
13	5	ord	$$⊢\phi \to \left(\neg U\in A\to U=\left\{\underset{\dot{}}{0}\right\}\right)$$
14	13	necon1ad	$$⊢\phi \to \left(U\ne \left\{\underset{\dot{}}{0}\right\}\to U\in A\right)$$
15	14	adantr	$$⊢\left(\phi \wedge T\subseteq U\right)\to \left(U\ne \left\{\underset{\dot{}}{0}\right\}\to U\in A\right)$$
16	12 15	mpd	$$⊢\left(\phi \wedge T\subseteq U\right)\to U\in A$$
17	2 7 8 16	lsatcmp	$$⊢\left(\phi \wedge T\subseteq U\right)\to \left(T\subseteq U\leftrightarrow T=U\right)$$
18	6 17	mpbid	$$⊢\left(\phi \wedge T\subseteq U\right)\to T=U$$
19	18	ex	$$⊢\phi \to \left(T\subseteq U\to T=U\right)$$
20		eqimss	$$⊢T=U\to T\subseteq U$$
21	19 20	impbid1	$$⊢\phi \to \left(T\subseteq U\leftrightarrow T=U\right)$$