Theorem ople0

Description: An element less than or equal to zero equals zero. ( chle0 analog.) (Contributed by NM, 21-Oct-2011)

	Ref	Expression
Hypotheses	op0le.b	|- B = ( Base ` K )
	op0le.l	|- .<_ = ( le ` K )
	op0le.z	|- .0. = ( 0. ` K )
Assertion	ople0	|- ( ( K e. OP /\ X e. B ) -> ( X .<_ .0. <-> X = .0. ) )

Proof

Step	Hyp	Ref	Expression
1		op0le.b	|- B = ( Base ` K )
2		op0le.l	|- .<_ = ( le ` K )
3		op0le.z	|- .0. = ( 0. ` K )
4	1 2 3	op0le	|- ( ( K e. OP /\ X e. B ) -> .0. .<_ X )
5	4	biantrud	|- ( ( K e. OP /\ X e. B ) -> ( X .<_ .0. <-> ( X .<_ .0. /\ .0. .<_ X ) ) )
6		opposet	|- ( K e. OP -> K e. Poset )
7	6	adantr	|- ( ( K e. OP /\ X e. B ) -> K e. Poset )
8		simpr	|- ( ( K e. OP /\ X e. B ) -> X e. B )
9	1 3	op0cl	|- ( K e. OP -> .0. e. B )
10	9	adantr	|- ( ( K e. OP /\ X e. B ) -> .0. e. B )
11	1 2	posasymb	|- ( ( K e. Poset /\ X e. B /\ .0. e. B ) -> ( ( X .<_ .0. /\ .0. .<_ X ) <-> X = .0. ) )
12	7 8 10 11	syl3anc	|- ( ( K e. OP /\ X e. B ) -> ( ( X .<_ .0. /\ .0. .<_ X ) <-> X = .0. ) )
13	5 12	bitrd	|- ( ( K e. OP /\ X e. B ) -> ( X .<_ .0. <-> X = .0. ) )