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	⊢ 0 = ( 0g ‘ 𝑊 )
	lsatcmp2.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
	lsatcmp2.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lsatcmp2.t	⊢ ( 𝜑 → 𝑇 ∈ 𝐴 )
	lsatcmp2.u	⊢ ( 𝜑 → ( 𝑈 ∈ 𝐴 ∨ 𝑈 = { 0 } ) )
Assertion	lsatcmp2	⊢ ( 𝜑 → ( 𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		lsatcmp2.o	⊢ 0 = ( 0g ‘ 𝑊 )
2		lsatcmp2.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
3		lsatcmp2.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
4		lsatcmp2.t	⊢ ( 𝜑 → 𝑇 ∈ 𝐴 )
5		lsatcmp2.u	⊢ ( 𝜑 → ( 𝑈 ∈ 𝐴 ∨ 𝑈 = { 0 } ) )
6		simpr	⊢ ( ( 𝜑 ∧ 𝑇 ⊆ 𝑈 ) → 𝑇 ⊆ 𝑈 )
7	3	adantr	⊢ ( ( 𝜑 ∧ 𝑇 ⊆ 𝑈 ) → 𝑊 ∈ LVec )
8	4	adantr	⊢ ( ( 𝜑 ∧ 𝑇 ⊆ 𝑈 ) → 𝑇 ∈ 𝐴 )
9		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
10	3 9	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
11	10	adantr	⊢ ( ( 𝜑 ∧ 𝑇 ⊆ 𝑈 ) → 𝑊 ∈ LMod )
12	1 2 11 8 6	lsatssn0	⊢ ( ( 𝜑 ∧ 𝑇 ⊆ 𝑈 ) → 𝑈 ≠ { 0 } )
13	5	ord	⊢ ( 𝜑 → ( ¬ 𝑈 ∈ 𝐴 → 𝑈 = { 0 } ) )
14	13	necon1ad	⊢ ( 𝜑 → ( 𝑈 ≠ { 0 } → 𝑈 ∈ 𝐴 ) )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝑇 ⊆ 𝑈 ) → ( 𝑈 ≠ { 0 } → 𝑈 ∈ 𝐴 ) )
16	12 15	mpd	⊢ ( ( 𝜑 ∧ 𝑇 ⊆ 𝑈 ) → 𝑈 ∈ 𝐴 )
17	2 7 8 16	lsatcmp	⊢ ( ( 𝜑 ∧ 𝑇 ⊆ 𝑈 ) → ( 𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈 ) )
18	6 17	mpbid	⊢ ( ( 𝜑 ∧ 𝑇 ⊆ 𝑈 ) → 𝑇 = 𝑈 )
19	18	ex	⊢ ( 𝜑 → ( 𝑇 ⊆ 𝑈 → 𝑇 = 𝑈 ) )
20		eqimss	⊢ ( 𝑇 = 𝑈 → 𝑇 ⊆ 𝑈 )
21	19 20	impbid1	⊢ ( 𝜑 → ( 𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈 ) )