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 = ( Base ` K )
	leatom.l	|- .<_ = ( le ` K )
	leatom.z	|- .0. = ( 0. ` K )
	leatom.a	|- A = ( Atoms ` K )
Assertion	leat2	|- ( ( ( K e. OP /\ X e. B /\ P e. A ) /\ ( X =/= .0. /\ X .<_ P ) ) -> X = P )

Proof

Step	Hyp	Ref	Expression
1		leatom.b	|- B = ( Base ` K )
2		leatom.l	|- .<_ = ( le ` K )
3		leatom.z	|- .0. = ( 0. ` K )
4		leatom.a	|- A = ( Atoms ` K )
5	1 2 3 4	leatb	|- ( ( K e. OP /\ X e. B /\ P e. A ) -> ( X .<_ P <-> ( X = P \/ X = .0. ) ) )
6		orcom	|- ( ( X = P \/ X = .0. ) <-> ( X = .0. \/ X = P ) )
7		neor	|- ( ( X = .0. \/ X = P ) <-> ( X =/= .0. -> X = P ) )
8	6 7	bitri	|- ( ( X = P \/ X = .0. ) <-> ( X =/= .0. -> X = P ) )
9	5 8	bitrdi	|- ( ( K e. OP /\ X e. B /\ P e. A ) -> ( X .<_ P <-> ( X =/= .0. -> X = P ) ) )
10	9	biimpd	|- ( ( K e. OP /\ X e. B /\ P e. A ) -> ( X .<_ P -> ( X =/= .0. -> X = P ) ) )
11	10	com23	|- ( ( K e. OP /\ X e. B /\ P e. A ) -> ( X =/= .0. -> ( X .<_ P -> X = P ) ) )
12	11	imp32	|- ( ( ( K e. OP /\ X e. B /\ P e. A ) /\ ( X =/= .0. /\ X .<_ P ) ) -> X = P )