Theorem atnle0

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

	Ref	Expression
Hypotheses	atnle0.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	atnle0.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	atnle0.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	atnle0	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\right)\to \neg P\underset{\dot{}}{\le }\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		atnle0.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		atnle0.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
3		atnle0.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		atlpos	$$⊢K\in \mathrm{AtLat}\to K\in \mathrm{Poset}$$
5	4	adantr	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\right)\to K\in \mathrm{Poset}$$
6		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
7	6 2	atl0cl	$$⊢K\in \mathrm{AtLat}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_K$$
8	7	adantr	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\right)\to \underset{\dot{}}{0}\in {\mathrm{Base}}_K$$
9	6 3	atbase	$$⊢P\in A\to P\in {\mathrm{Base}}_K$$
10	9	adantl	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\right)\to P\in {\mathrm{Base}}_K$$
11		eqid	$$⊢{⋖}_K={⋖}_K$$
12	2 11 3	atcvr0	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\right)\to \underset{\dot{}}{0}{⋖}_{K}P$$
13	6 1 11	cvrnle	$$⊢\left(\left(K\in \mathrm{Poset}\wedge \underset{\dot{}}{0}\in {\mathrm{Base}}_K\wedge P\in {\mathrm{Base}}_K\right)\wedge \underset{\dot{}}{0}{⋖}_{K}P\right)\to \neg P\underset{\dot{}}{\le }\underset{\dot{}}{0}$$
14	5 8 10 12 13	syl31anc	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\right)\to \neg P\underset{\dot{}}{\le }\underset{\dot{}}{0}$$