Metamath Proof Explorer

Theorem 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 ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
doch11.k ⊢ φ → K ∈ HL ∧ W ∈ H
doch11.x ⊢ φ → X ∈ ran ⁡ I
doch11.y ⊢ φ → Y ∈ ran ⁡ I
Assertion dochsordN ⊢ φ → X ⊂ Y ↔ ⊥ ˙ ⁡ Y ⊂ ⊥ ˙ ⁡ X

Proof

Step Hyp Ref Expression
1 doch11.h ⊢ H = LHyp ⁡ K
2 doch11.i ⊢ I = DIsoH ⁡ K ⁡ W
3 doch11.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
4 doch11.k ⊢ φ → K ∈ HL ∧ W ∈ H
5 doch11.x ⊢ φ → X ∈ ran ⁡ I
6 doch11.y ⊢ φ → Y ∈ ran ⁡ I
7 1 2 3 4 5 6 dochord ⊢ φ → X ⊆ Y ↔ ⊥ ˙ ⁡ Y ⊆ ⊥ ˙ ⁡ X
8 1 2 3 4 6 5 doch11 ⊢ φ → ⊥ ˙ ⁡ Y = ⊥ ˙ ⁡ X ↔ Y = X
9 eqcom ⊢ Y = X ↔ X = Y
10 8 9 bitr2di ⊢ φ → X = Y ↔ ⊥ ˙ ⁡ Y = ⊥ ˙ ⁡ X
11 10 necon3bid ⊢ φ → X ≠ Y ↔ ⊥ ˙ ⁡ Y ≠ ⊥ ˙ ⁡ X
12 7 11 anbi12d ⊢ φ → X ⊆ Y ∧ X ≠ Y ↔ ⊥ ˙ ⁡ Y ⊆ ⊥ ˙ ⁡ X ∧ ⊥ ˙ ⁡ Y ≠ ⊥ ˙ ⁡ X
13 df-pss ⊢ X ⊂ Y ↔ X ⊆ Y ∧ X ≠ Y
14 df-pss ⊢ ⊥ ˙ ⁡ Y ⊂ ⊥ ˙ ⁡ X ↔ ⊥ ˙ ⁡ Y ⊆ ⊥ ˙ ⁡ X ∧ ⊥ ˙ ⁡ Y ≠ ⊥ ˙ ⁡ X
15 12 13 14 3bitr4g ⊢ φ → X ⊂ Y ↔ ⊥ ˙ ⁡ Y ⊂ ⊥ ˙ ⁡ X