oplecon3

Description: Contraposition law for orthoposets. (Contributed by NM, 13-Sep-2011)

	Ref	Expression
Hypotheses	opcon3.b	$⊢ B = {Base}_{K}$
	opcon3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	opcon3.o	$⊢ \underset{˙}{⊥} = oc (K)$
Assertion	oplecon3	$⊢ (K \in OP \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \to \underset{˙}{⊥} (Y) \underset{˙}{\leq} \underset{˙}{⊥} (X))$

Step	Hyp	Ref	Expression
1		opcon3.b	$⊢ B = {Base}_{K}$
2		opcon3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		opcon3.o	$⊢ \underset{˙}{⊥} = oc (K)$
4		eqid	$⊢ join (K) = join (K)$
5		eqid	$⊢ meet (K) = meet (K)$
6		eqid	$⊢ 0. (K) = 0. (K)$
7		eqid	$⊢ 1. (K) = 1. (K)$
8	1 2 3 4 5 6 7	oposlem	$⊢ (K \in OP \land X \in B \land Y \in B) \to ((\underset{˙}{⊥} (X) \in B \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land (X \underset{˙}{\leq} Y \to \underset{˙}{⊥} (Y) \underset{˙}{\leq} \underset{˙}{⊥} (X))) \land X join (K) \underset{˙}{⊥} (X) = 1. (K) \land X meet (K) \underset{˙}{⊥} (X) = 0. (K))$
9	8	simp1d	$⊢ (K \in OP \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (X) \in B \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land (X \underset{˙}{\leq} Y \to \underset{˙}{⊥} (Y) \underset{˙}{\leq} \underset{˙}{⊥} (X)))$
10	9	simp3d	$⊢ (K \in OP \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \to \underset{˙}{⊥} (Y) \underset{˙}{\leq} \underset{˙}{⊥} (X))$

Metamath Proof Explorer