This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈 ) )