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{˙}{0} = 0_{W}$
	lsatcmp2.a	$⊢ A = LSAtoms (W)$
	lsatcmp2.w	$⊢ φ \to W \in LVec$
	lsatcmp2.t	$⊢ φ \to T \in A$
	lsatcmp2.u	$⊢ φ \to (U \in A \lor U = \{\underset{˙}{0}\})$
Assertion	lsatcmp2	$⊢ φ \to (T \subseteq U \leftrightarrow T = U)$

Proof

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

Metamath Proof Explorer

Theorem lsatcmp2

Proof