opcon3b

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

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

Step	Hyp	Ref	Expression
1		opoccl.b	$⊢ B = {Base}_{K}$
2		opoccl.o	$⊢ \underset{˙}{⊥} = oc (K)$
3		fveq2	$⊢ Y = X \to \underset{˙}{⊥} (Y) = \underset{˙}{⊥} (X)$
4	3	eqcoms	$⊢ X = Y \to \underset{˙}{⊥} (Y) = \underset{˙}{⊥} (X)$
5		fveq2	$⊢ \underset{˙}{⊥} (X) = \underset{˙}{⊥} (Y) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = \underset{˙}{⊥} (\underset{˙}{⊥} (Y))$
6	5	eqcoms	$⊢ \underset{˙}{⊥} (Y) = \underset{˙}{⊥} (X) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = \underset{˙}{⊥} (\underset{˙}{⊥} (Y))$
7	1 2	opococ	$⊢ (K \in OP \land X \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
8	7	3adant3	$⊢ (K \in OP \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
9	1 2	opococ	$⊢ (K \in OP \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y$
10	9	3adant2	$⊢ (K \in OP \land X \in B \land Y \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y$
11	8 10	eqeq12d	$⊢ (K \in OP \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) \leftrightarrow X = Y)$
12	6 11	syl5ib	$⊢ (K \in OP \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (Y) = \underset{˙}{⊥} (X) \to X = Y)$
13	4 12	impbid2	$⊢ (K \in OP \land X \in B \land Y \in B) \to (X = Y \leftrightarrow \underset{˙}{⊥} (Y) = \underset{˙}{⊥} (X))$

Metamath Proof Explorer