Metamath Proof Explorer

Theorem opcon2b

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

Ref Expression
Hypotheses opoccl.b ⊢ B = Base K
opoccl.o ⊢ ⊥ ˙ = oc ⁡ K
Assertion opcon2b ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B → X = ⊥ ˙ ⁡ Y ↔ Y = ⊥ ˙ ⁡ X

Proof

Step Hyp Ref Expression
1 opoccl.b ⊢ B = Base K
2 opoccl.o ⊢ ⊥ ˙ = oc ⁡ K
3 1 2 opoccl ⊢ K ∈ OP ∧ Y ∈ B → ⊥ ˙ ⁡ Y ∈ B
4 3 3adant2 ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B → ⊥ ˙ ⁡ Y ∈ B
5 1 2 opcon3b ⊢ K ∈ OP ∧ X ∈ B ∧ ⊥ ˙ ⁡ Y ∈ B → X = ⊥ ˙ ⁡ Y ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y = ⊥ ˙ ⁡ X
6 4 5 syld3an3 ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B → X = ⊥ ˙ ⁡ Y ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y = ⊥ ˙ ⁡ X
7 1 2 opococ ⊢ K ∈ OP ∧ Y ∈ B → ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y = Y
8 7 3adant2 ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B → ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y = Y
9 8 eqeq1d ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B → ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y = ⊥ ˙ ⁡ X ↔ Y = ⊥ ˙ ⁡ X
10 6 9 bitrd ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B → X = ⊥ ˙ ⁡ Y ↔ Y = ⊥ ˙ ⁡ X