Theorem leat

Description: A poset element less than or equal to an atom equals either zero or the atom. (Contributed by NM, 15-Oct-2013)

	Ref	Expression
Hypotheses	leatom.b	$$⊢B={\mathrm{Base}}_K$$
	leatom.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	leatom.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	leatom.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	leat	$$⊢\left(\left(K\in \mathrm{OP}\wedge X\in B\wedge P\in A\right)\wedge X\underset{\dot{}}{\le }P\right)\to \left(X=P\vee X=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		leatom.b	$$⊢B={\mathrm{Base}}_K$$
2		leatom.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		leatom.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
4		leatom.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5	1 2 3 4	leatb	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\wedge P\in A\right)\to \left(X\underset{\dot{}}{\le }P\leftrightarrow \left(X=P\vee X=\underset{\dot{}}{0}\right)\right)$$
6	5	biimpa	$$⊢\left(\left(K\in \mathrm{OP}\wedge X\in B\wedge P\in A\right)\wedge X\underset{\dot{}}{\le }P\right)\to \left(X=P\vee X=\underset{\dot{}}{0}\right)$$