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	$⊢ \underset{˙}{\leq} = \leq_{K}$
	atl0le.z	$⊢ \underset{˙}{0} = 0. (K)$
Assertion	atl0le	$⊢ (K \in AtLat \land X \in B) \to \underset{˙}{0} \underset{˙}{\leq} X$

Step	Hyp	Ref	Expression
1		atl0le.b	$⊢ B = {Base}_{K}$
2		atl0le.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		atl0le.z	$⊢ \underset{˙}{0} = 0. (K)$
4		eqid	$⊢ glb (K) = glb (K)$
5		simpl	$⊢ (K \in AtLat \land X \in B) \to K \in AtLat$
6		simpr	$⊢ (K \in AtLat \land X \in B) \to X \in B$
7		eqid	$⊢ lub (K) = lub (K)$
8	1 7 4	atl0dm	$⊢ K \in AtLat \to B \in dom glb (K)$
9	8	adantr	$⊢ (K \in AtLat \land X \in B) \to B \in dom glb (K)$
10	1 4 2 3 5 6 9	p0le	$⊢ (K \in AtLat \land X \in B) \to \underset{˙}{0} \underset{˙}{\leq} X$

Metamath Proof Explorer