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

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

Metamath Proof Explorer