opcon1b

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

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

Step	Hyp	Ref	Expression
1		opoccl.b	$⊢ B = {Base}_{K}$
2		opoccl.o	$⊢ \underset{˙}{⊥} = oc (K)$
3	1 2	opcon2b	$⊢ (K \in OP \land X \in B \land Y \in B) \to (X = \underset{˙}{⊥} (Y) \leftrightarrow Y = \underset{˙}{⊥} (X))$
4		eqcom	$⊢ \underset{˙}{⊥} (Y) = X \leftrightarrow X = \underset{˙}{⊥} (Y)$
5		eqcom	$⊢ \underset{˙}{⊥} (X) = Y \leftrightarrow Y = \underset{˙}{⊥} (X)$
6	3 4 5	3bitr4g	$⊢ (K \in OP \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (Y) = X \leftrightarrow \underset{˙}{⊥} (X) = Y)$
7	6	bicomd	$⊢ (K \in OP \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (X) = Y \leftrightarrow \underset{˙}{⊥} (Y) = X)$

Metamath Proof Explorer