Theorem atl0le

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

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

Proof

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