Theorem op0le

Description: Orthoposet zero is less than or equal to any element. ( ch0le analog.) (Contributed by NM, 12-Oct-2011)

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

Proof

Step	Hyp	Ref	Expression
1		op0le.b	|- B = ( Base ` K )
2		op0le.l	|- .<_ = ( le ` K )
3		op0le.z	|- .0. = ( 0. ` K )
4		eqid	|- ( glb ` K ) = ( glb ` K )
5		simpl	|- ( ( K e. OP /\ X e. B ) -> K e. OP )
6		simpr	|- ( ( K e. OP /\ X e. B ) -> X e. B )
7		eqid	|- ( lub ` K ) = ( lub ` K )
8	1 7 4	op01dm	|- ( K e. OP -> ( B e. dom ( lub ` K ) /\ B e. dom ( glb ` K ) ) )
9	8	simprd	|- ( K e. OP -> B e. dom ( glb ` K ) )
10	9	adantr	|- ( ( K e. OP /\ X e. B ) -> B e. dom ( glb ` K ) )
11	1 4 2 3 5 6 10	p0le	|- ( ( K e. OP /\ X e. B ) -> .0. .<_ X )