opltcon2b

Description: Contraposition law for strict ordering in orthoposets. ( chsscon2 analog.) (Contributed by NM, 5-Nov-2011)

	Ref	Expression
Hypotheses	opltcon3.b	$⊢ B = {Base}_{K}$
	opltcon3.s	$⊢ \underset{˙}{<} = <_{K}$
	opltcon3.o	$⊢ \underset{˙}{⊥} = oc (K)$
Assertion	opltcon2b	$⊢ (K \in OP \land X \in B \land Y \in B) \to (X \underset{˙}{<} \underset{˙}{⊥} (Y) \leftrightarrow Y \underset{˙}{<} \underset{˙}{⊥} (X))$

Step	Hyp	Ref	Expression
1		opltcon3.b	$⊢ B = {Base}_{K}$
2		opltcon3.s	$⊢ \underset{˙}{<} = <_{K}$
3		opltcon3.o	$⊢ \underset{˙}{⊥} = oc (K)$
4	1 3	opoccl	$⊢ (K \in OP \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
5	4	3adant2	$⊢ (K \in OP \land X \in B \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
6	1 2 3	opltcon3b	$⊢ (K \in OP \land X \in B \land \underset{˙}{⊥} (Y) \in B) \to (X \underset{˙}{<} \underset{˙}{⊥} (Y) \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) \underset{˙}{<} \underset{˙}{⊥} (X))$
7	5 6	syld3an3	$⊢ (K \in OP \land X \in B \land Y \in B) \to (X \underset{˙}{<} \underset{˙}{⊥} (Y) \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) \underset{˙}{<} \underset{˙}{⊥} (X))$
8	1 3	opococ	$⊢ (K \in OP \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y$
9	8	3adant2	$⊢ (K \in OP \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y$
10	9	breq1d	$⊢ (K \in OP \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (Y)) \underset{˙}{<} \underset{˙}{⊥} (X) \leftrightarrow Y \underset{˙}{<} \underset{˙}{⊥} (X))$
11	7 10	bitrd	$⊢ (K \in OP \land X \in B \land Y \in B) \to (X \underset{˙}{<} \underset{˙}{⊥} (Y) \leftrightarrow Y \underset{˙}{<} \underset{˙}{⊥} (X))$

Metamath Proof Explorer