opcon2b

Description: Orthocomplement contraposition law. ( negcon2 analog.) (Contributed by NM, 16-Jan-2012)

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

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

Metamath Proof Explorer