ople1

Description: Any element is less than the orthoposet unity. ( chss analog.) (Contributed by NM, 23-Oct-2011)

	Ref	Expression
Hypotheses	ople1.b	$⊢ B = {Base}_{K}$
	ople1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	ople1.u	$⊢ \underset{˙}{1} = 1. (K)$
Assertion	ople1	$⊢ (K \in OP \land X \in B) \to X \underset{˙}{\leq} \underset{˙}{1}$

Step	Hyp	Ref	Expression
1		ople1.b	$⊢ B = {Base}_{K}$
2		ople1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		ople1.u	$⊢ \underset{˙}{1} = 1. (K)$
4		eqid	$⊢ lub (K) = lub (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	$⊢ glb (K) = glb (K)$
8	1 4 7	op01dm	$⊢ K \in OP \to (B \in dom lub (K) \land B \in dom glb (K))$
9	8	simpld	$⊢ K \in OP \to B \in dom lub (K)$
10	9	adantr	$⊢ (K \in OP \land X \in B) \to B \in dom lub (K)$
11	1 4 2 3 5 6 10	ple1	$⊢ (K \in OP \land X \in B) \to X \underset{˙}{\leq} \underset{˙}{1}$

Metamath Proof Explorer