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

Metamath Proof Explorer

Theorem atnle0

Description: An atom is not less than or equal to zero. (Contributed by NM, 17-Oct-2011)

Ref Expression
Hypotheses atnle0.l ⊢ ≤ = ( le ‘ 𝐾 )
atnle0.z ⊢ 0 = ( 0. ‘ 𝐾 )
atnle0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion atnle0 ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ) → ¬ 𝑃 ≤ 0 )

Proof

Step Hyp Ref Expression
1 atnle0.l ⊢ ≤ = ( le ‘ 𝐾 )
2 atnle0.z ⊢ 0 = ( 0. ‘ 𝐾 )
3 atnle0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 atlpos ⊢ ( 𝐾 ∈ AtLat → 𝐾 ∈ Poset )
5 4 adantr ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ) → 𝐾 ∈ Poset )
6 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7 6 2 atl0cl ⊢ ( 𝐾 ∈ AtLat → 0 ∈ ( Base ‘ 𝐾 ) )
8 7 adantr ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ) → 0 ∈ ( Base ‘ 𝐾 ) )
9 6 3 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
10 9 adantl ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
11 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
12 2 11 3 atcvr0 ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ) → 0 ( ⋖ ‘ 𝐾 ) 𝑃 )
13 6 1 11 cvrnle ⊢ ( ( ( 𝐾 ∈ Poset ∧ 0 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) ∧ 0 ( ⋖ ‘ 𝐾 ) 𝑃 ) → ¬ 𝑃 ≤ 0 )
14 5 8 10 12 13 syl31anc ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ) → ¬ 𝑃 ≤ 0 )