Metamath Proof Explorer

Theorem oplecon3b

Description: Contraposition law for orthoposets. ( chsscon3 analog.) (Contributed by NM, 4-Nov-2011)

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

Proof

Step	Hyp	Ref	Expression
1		opcon3.b	$⊢ B = {Base}_{K}$
2		opcon3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		opcon3.o	$⊢ \underset{˙}{⊥} = oc (K)$
4	1 2 3	oplecon3	$⊢ (K \in OP \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \to \underset{˙}{⊥} (Y) \underset{˙}{\leq} \underset{˙}{⊥} (X))$
5		simp1	$⊢ (K \in OP \land X \in B \land Y \in B) \to K \in OP$
6	1 3	opoccl	$⊢ (K \in OP \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
7	6	3adant2	$⊢ (K \in OP \land X \in B \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
8	1 3	opoccl	$⊢ (K \in OP \land X \in B) \to \underset{˙}{⊥} (X) \in B$
9	8	3adant3	$⊢ (K \in OP \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X) \in B$
10	1 2 3	oplecon3	$⊢ (K \in OP \land \underset{˙}{⊥} (Y) \in B \land \underset{˙}{⊥} (X) \in B) \to (\underset{˙}{⊥} (Y) \underset{˙}{\leq} \underset{˙}{⊥} (X) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \underset{˙}{\leq} \underset{˙}{⊥} (\underset{˙}{⊥} (Y)))$
11	5 7 9 10	syl3anc	$⊢ (K \in OP \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (Y) \underset{˙}{\leq} \underset{˙}{⊥} (X) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \underset{˙}{\leq} \underset{˙}{⊥} (\underset{˙}{⊥} (Y)))$
12	1 3	opococ	$⊢ (K \in OP \land X \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
13	12	3adant3	$⊢ (K \in OP \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
14	1 3	opococ	$⊢ (K \in OP \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y$
15	14	3adant2	$⊢ (K \in OP \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y$
16	13 15	breq12d	$⊢ (K \in OP \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) \underset{˙}{\leq} \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) \leftrightarrow X \underset{˙}{\leq} Y)$
17	11 16	sylibd	$⊢ (K \in OP \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (Y) \underset{˙}{\leq} \underset{˙}{⊥} (X) \to X \underset{˙}{\leq} Y)$
18	4 17	impbid	$⊢ (K \in OP \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \leftrightarrow \underset{˙}{⊥} (Y) \underset{˙}{\leq} \underset{˙}{⊥} (X))$