opexmid

Description: Law of excluded middle for orthoposets. ( chjo analog.) (Contributed by NM, 13-Sep-2011)

	Ref	Expression
Hypotheses	opexmid.b	$⊢ B = {Base}_{K}$
	opexmid.o	$⊢ \underset{˙}{⊥} = oc (K)$
	opexmid.j	$⊢ \underset{˙}{\lor} = join (K)$
	opexmid.u	$⊢ \underset{˙}{1} = 1. (K)$
Assertion	opexmid	$⊢ (K \in OP \land X \in B) \to X \underset{˙}{\lor} \underset{˙}{⊥} (X) = \underset{˙}{1}$

Step	Hyp	Ref	Expression
1		opexmid.b	$⊢ B = {Base}_{K}$
2		opexmid.o	$⊢ \underset{˙}{⊥} = oc (K)$
3		opexmid.j	$⊢ \underset{˙}{\lor} = join (K)$
4		opexmid.u	$⊢ \underset{˙}{1} = 1. (K)$
5		eqid	$⊢ \leq_{K} = \leq_{K}$
6		eqid	$⊢ meet (K) = meet (K)$
7		eqid	$⊢ 0. (K) = 0. (K)$
8	1 5 2 3 6 7 4	oposlem	$⊢ (K \in OP \land X \in B \land X \in B) \to ((\underset{˙}{⊥} (X) \in B \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land (X \leq_{K} X \to \underset{˙}{⊥} (X) \leq_{K} \underset{˙}{⊥} (X))) \land X \underset{˙}{\lor} \underset{˙}{⊥} (X) = \underset{˙}{1} \land X meet (K) \underset{˙}{⊥} (X) = 0. (K))$
9	8	3anidm23	$⊢ (K \in OP \land X \in B) \to ((\underset{˙}{⊥} (X) \in B \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land (X \leq_{K} X \to \underset{˙}{⊥} (X) \leq_{K} \underset{˙}{⊥} (X))) \land X \underset{˙}{\lor} \underset{˙}{⊥} (X) = \underset{˙}{1} \land X meet (K) \underset{˙}{⊥} (X) = 0. (K))$
10	9	simp2d	$⊢ (K \in OP \land X \in B) \to X \underset{˙}{\lor} \underset{˙}{⊥} (X) = \underset{˙}{1}$

Metamath Proof Explorer