Theorem leat2

Description: A nonzero poset element less than or equal to an atom equals the atom. (Contributed by NM, 6-Mar-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	leat2	$$⊢\left(\left(K\in \mathrm{OP}\wedge X\in B\wedge P\in A\right)\wedge \left(X\ne \underset{\dot{}}{0}\wedge X\underset{\dot{}}{\le }P\right)\right)\to X=P$$

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		orcom	$$⊢\left(X=P\vee X=\underset{\dot{}}{0}\right)\leftrightarrow \left(X=\underset{\dot{}}{0}\vee X=P\right)$$
7		neor	$$⊢\left(X=\underset{\dot{}}{0}\vee X=P\right)\leftrightarrow \left(X\ne \underset{\dot{}}{0}\to X=P\right)$$
8	6 7	bitri	$$⊢\left(X=P\vee X=\underset{\dot{}}{0}\right)\leftrightarrow \left(X\ne \underset{\dot{}}{0}\to X=P\right)$$
9	5 8	syl6bb	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\wedge P\in A\right)\to \left(X\underset{\dot{}}{\le }P\leftrightarrow \left(X\ne \underset{\dot{}}{0}\to X=P\right)\right)$$
10	9	biimpd	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\wedge P\in A\right)\to \left(X\underset{\dot{}}{\le }P\to \left(X\ne \underset{\dot{}}{0}\to X=P\right)\right)$$
11	10	com23	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\wedge P\in A\right)\to \left(X\ne \underset{\dot{}}{0}\to \left(X\underset{\dot{}}{\le }P\to X=P\right)\right)$$
12	11	imp32	$$⊢\left(\left(K\in \mathrm{OP}\wedge X\in B\wedge P\in A\right)\wedge \left(X\ne \underset{\dot{}}{0}\wedge X\underset{\dot{}}{\le }P\right)\right)\to X=P$$