opnoncon

Description: Law of contradiction for orthoposets. ( chocin analog.) (Contributed by NM, 13-Sep-2011)

	Ref	Expression
Hypotheses	opnoncon.b	$⊢ B = {Base}_{K}$
	opnoncon.o	$⊢ \underset{˙}{⊥} = oc (K)$
	opnoncon.m	$⊢ \underset{˙}{\land} = meet (K)$
	opnoncon.z	$⊢ \underset{˙}{0} = 0. (K)$
Assertion	opnoncon	$⊢ (K \in OP \land X \in B) \to X \underset{˙}{\land} \underset{˙}{⊥} (X) = \underset{˙}{0}$

Step	Hyp	Ref	Expression
1		opnoncon.b	$⊢ B = {Base}_{K}$
2		opnoncon.o	$⊢ \underset{˙}{⊥} = oc (K)$
3		opnoncon.m	$⊢ \underset{˙}{\land} = meet (K)$
4		opnoncon.z	$⊢ \underset{˙}{0} = 0. (K)$
5		eqid	$⊢ \leq_{K} = \leq_{K}$
6		eqid	$⊢ join (K) = join (K)$
7		eqid	$⊢ 1. (K) = 1. (K)$
8	1 5 2 6 3 4 7	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 join (K) \underset{˙}{⊥} (X) = 1. (K) \land X \underset{˙}{\land} \underset{˙}{⊥} (X) = \underset{˙}{0})$
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 join (K) \underset{˙}{⊥} (X) = 1. (K) \land X \underset{˙}{\land} \underset{˙}{⊥} (X) = \underset{˙}{0})$
10	9	simp3d	$⊢ (K \in OP \land X \in B) \to X \underset{˙}{\land} \underset{˙}{⊥} (X) = \underset{˙}{0}$

Metamath Proof Explorer