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 )