opltcon3b

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

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

Proof

Step	Hyp	Ref	Expression
1		opltcon3.b	$⊢ B = {Base}_{K}$
2		opltcon3.s	$⊢ \underset{˙}{<} = <_{K}$
3		opltcon3.o	$⊢ \underset{˙}{⊥} = oc (K)$
4		eqid	$⊢ \leq_{K} = \leq_{K}$
5	1 4 3	oplecon3b	$⊢ (K \in OP \land X \in B \land Y \in B) \to (X \leq_{K} Y \leftrightarrow \underset{˙}{⊥} (Y) \leq_{K} \underset{˙}{⊥} (X))$
6	1 4 3	oplecon3b	$⊢ (K \in OP \land Y \in B \land X \in B) \to (Y \leq_{K} X \leftrightarrow \underset{˙}{⊥} (X) \leq_{K} \underset{˙}{⊥} (Y))$
7	6	3com23	$⊢ (K \in OP \land X \in B \land Y \in B) \to (Y \leq_{K} X \leftrightarrow \underset{˙}{⊥} (X) \leq_{K} \underset{˙}{⊥} (Y))$
8	7	notbid	$⊢ (K \in OP \land X \in B \land Y \in B) \to (\neg Y \leq_{K} X \leftrightarrow \neg \underset{˙}{⊥} (X) \leq_{K} \underset{˙}{⊥} (Y))$
9	5 8	anbi12d	$⊢ (K \in OP \land X \in B \land Y \in B) \to ((X \leq_{K} Y \land \neg Y \leq_{K} X) \leftrightarrow (\underset{˙}{⊥} (Y) \leq_{K} \underset{˙}{⊥} (X) \land \neg \underset{˙}{⊥} (X) \leq_{K} \underset{˙}{⊥} (Y)))$
10		opposet	$⊢ K \in OP \to K \in Poset$
11	1 4 2	pltval3	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \leftrightarrow (X \leq_{K} Y \land \neg Y \leq_{K} X))$
12	10 11	syl3an1	$⊢ (K \in OP \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \leftrightarrow (X \leq_{K} Y \land \neg Y \leq_{K} X))$
13	10	3ad2ant1	$⊢ (K \in OP \land X \in B \land Y \in B) \to K \in Poset$
14	1 3	opoccl	$⊢ (K \in OP \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
15	14	3adant2	$⊢ (K \in OP \land X \in B \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
16	1 3	opoccl	$⊢ (K \in OP \land X \in B) \to \underset{˙}{⊥} (X) \in B$
17	16	3adant3	$⊢ (K \in OP \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X) \in B$
18	1 4 2	pltval3	$⊢ (K \in Poset \land \underset{˙}{⊥} (Y) \in B \land \underset{˙}{⊥} (X) \in B) \to (\underset{˙}{⊥} (Y) \underset{˙}{<} \underset{˙}{⊥} (X) \leftrightarrow (\underset{˙}{⊥} (Y) \leq_{K} \underset{˙}{⊥} (X) \land \neg \underset{˙}{⊥} (X) \leq_{K} \underset{˙}{⊥} (Y)))$
19	13 15 17 18	syl3anc	$⊢ (K \in OP \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (Y) \underset{˙}{<} \underset{˙}{⊥} (X) \leftrightarrow (\underset{˙}{⊥} (Y) \leq_{K} \underset{˙}{⊥} (X) \land \neg \underset{˙}{⊥} (X) \leq_{K} \underset{˙}{⊥} (Y)))$
20	9 12 19	3bitr4d	$⊢ (K \in OP \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \leftrightarrow \underset{˙}{⊥} (Y) \underset{˙}{<} \underset{˙}{⊥} (X))$

Metamath Proof Explorer

Theorem opltcon3b

Proof