Theorem op1le

Description: If the orthoposet unity is less than or equal to an element, the element equals the unit. ( chle0 analog.) (Contributed by NM, 5-Dec-2011)

	Ref	Expression
Hypotheses	ople1.b	|- B = ( Base ` K )
	ople1.l	|- .<_ = ( le ` K )
	ople1.u	|- .1. = ( 1. ` K )
Assertion	op1le	|- ( ( K e. OP /\ X e. B ) -> ( .1. .<_ X <-> X = .1. ) )

Proof

Step	Hyp	Ref	Expression
1		ople1.b	|- B = ( Base ` K )
2		ople1.l	|- .<_ = ( le ` K )
3		ople1.u	|- .1. = ( 1. ` K )
4	1 2 3	ople1	|- ( ( K e. OP /\ X e. B ) -> X .<_ .1. )
5	4	biantrurd	|- ( ( K e. OP /\ X e. B ) -> ( .1. .<_ X <-> ( X .<_ .1. /\ .1. .<_ 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	op1cl	|- ( K e. OP -> .1. e. B )
10	9	adantr	|- ( ( K e. OP /\ X e. B ) -> .1. e. B )
11	1 2	posasymb	|- ( ( K e. Poset /\ X e. B /\ .1. e. B ) -> ( ( X .<_ .1. /\ .1. .<_ X ) <-> X = .1. ) )
12	7 8 10 11	syl3anc	|- ( ( K e. OP /\ X e. B ) -> ( ( X .<_ .1. /\ .1. .<_ X ) <-> X = .1. ) )
13	5 12	bitrd	|- ( ( K e. OP /\ X e. B ) -> ( .1. .<_ X <-> X = .1. ) )