dochsordN

Description: Strict ordering law for orthocomplement. (Contributed by NM, 12-Aug-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	doch11.h	$⊢ H = LHyp (K)$
	doch11.i	$⊢ I = DIsoH (K) (W)$
	doch11.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	doch11.k	$⊢ φ \to (K \in HL \land W \in H)$
	doch11.x	$⊢ φ \to X \in ran I$
	doch11.y	$⊢ φ \to Y \in ran I$
Assertion	dochsordN	$⊢ φ \to (X \subset Y \leftrightarrow \underset{˙}{⊥} (Y) \subset \underset{˙}{⊥} (X))$

Step	Hyp	Ref	Expression
1		doch11.h	$⊢ H = LHyp (K)$
2		doch11.i	$⊢ I = DIsoH (K) (W)$
3		doch11.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
4		doch11.k	$⊢ φ \to (K \in HL \land W \in H)$
5		doch11.x	$⊢ φ \to X \in ran I$
6		doch11.y	$⊢ φ \to Y \in ran I$
7	1 2 3 4 5 6	dochord	$⊢ φ \to (X \subseteq Y \leftrightarrow \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X))$
8	1 2 3 4 6 5	doch11	$⊢ φ \to (\underset{˙}{⊥} (Y) = \underset{˙}{⊥} (X) \leftrightarrow Y = X)$
9		eqcom	$⊢ Y = X \leftrightarrow X = Y$
10	8 9	bitr2di	$⊢ φ \to (X = Y \leftrightarrow \underset{˙}{⊥} (Y) = \underset{˙}{⊥} (X))$
11	10	necon3bid	$⊢ φ \to (X \neq Y \leftrightarrow \underset{˙}{⊥} (Y) \neq \underset{˙}{⊥} (X))$
12	7 11	anbi12d	$⊢ φ \to ((X \subseteq Y \land X \neq Y) \leftrightarrow (\underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X) \land \underset{˙}{⊥} (Y) \neq \underset{˙}{⊥} (X)))$
13		df-pss	$⊢ X \subset Y \leftrightarrow (X \subseteq Y \land X \neq Y)$
14		df-pss	$⊢ \underset{˙}{⊥} (Y) \subset \underset{˙}{⊥} (X) \leftrightarrow (\underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X) \land \underset{˙}{⊥} (Y) \neq \underset{˙}{⊥} (X))$
15	12 13 14	3bitr4g	$⊢ φ \to (X \subset Y \leftrightarrow \underset{˙}{⊥} (Y) \subset \underset{˙}{⊥} (X))$

Metamath Proof Explorer