opltcon1b

Description: Contraposition law for strict ordering in orthoposets. ( chpsscon1 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	opltcon1b	$⊢ (K \in OP \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (X) \underset{˙}{<} Y \leftrightarrow \underset{˙}{⊥} (Y) \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 X \in B) \to \underset{˙}{⊥} (X) \in B$
5	4	3adant3	$⊢ (K \in OP \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X) \in B$
6	1 2 3	opltcon3b	$⊢ (K \in OP \land \underset{˙}{⊥} (X) \in B \land Y \in B) \to (\underset{˙}{⊥} (X) \underset{˙}{<} Y \leftrightarrow \underset{˙}{⊥} (Y) \underset{˙}{<} \underset{˙}{⊥} (\underset{˙}{⊥} (X)))$
7	5 6	syld3an2	$⊢ (K \in OP \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (X) \underset{˙}{<} Y \leftrightarrow \underset{˙}{⊥} (Y) \underset{˙}{<} \underset{˙}{⊥} (\underset{˙}{⊥} (X)))$
8	1 3	opococ	$⊢ (K \in OP \land X \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
9	8	3adant3	$⊢ (K \in OP \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
10	9	breq2d	$⊢ (K \in OP \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (Y) \underset{˙}{<} \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \leftrightarrow \underset{˙}{⊥} (Y) \underset{˙}{<} X)$
11	7 10	bitrd	$⊢ (K \in OP \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (X) \underset{˙}{<} Y \leftrightarrow \underset{˙}{⊥} (Y) \underset{˙}{<} X)$

Metamath Proof Explorer