Theorem leat3

Description: A poset element less than or equal to an atom is either an atom or zero. (Contributed by NM, 2-Dec-2012)

	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	leat3	$$⊢\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\in A\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	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)$$
6		simpl3	$$⊢\left(\left(K\in \mathrm{OP}\wedge X\in B\wedge P\in A\right)\wedge X\underset{\dot{}}{\le }P\right)\to P\in A$$
7		eleq1a	$$⊢P\in A\to \left(X=P\to X\in A\right)$$
8	6 7	syl	$$⊢\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\to X\in A\right)$$
9	8	orim1d	$$⊢\left(\left(K\in \mathrm{OP}\wedge X\in B\wedge P\in A\right)\wedge X\underset{\dot{}}{\le }P\right)\to \left(\left(X=P\vee X=\underset{\dot{}}{0}\right)\to \left(X\in A\vee X=\underset{\dot{}}{0}\right)\right)$$
10	5 9	mpd	$$⊢\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\in A\vee X=\underset{\dot{}}{0}\right)$$