Metamath Proof Explorer


Theorem opcon1b

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

Ref Expression
Hypotheses opoccl.b B = Base K
opoccl.o ˙ = oc K
Assertion opcon1b 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 opcon2b K OP X B Y B X = ˙ Y Y = ˙ X
4 eqcom ˙ Y = X X = ˙ Y
5 eqcom ˙ X = Y Y = ˙ X
6 3 4 5 3bitr4g K OP X B Y B ˙ Y = X ˙ X = Y
7 6 bicomd K OP X B Y B ˙ X = Y ˙ Y = X