Metamath Proof Explorer


Theorem opoc0

Description: Orthocomplement of orthoposet zero. (Contributed by NM, 24-Jan-2012)

Ref Expression
Hypotheses opoc1.z 0˙=0.K
opoc1.u 1˙=1.K
opoc1.o ˙=ocK
Assertion opoc0 KOP˙0˙=1˙

Proof

Step Hyp Ref Expression
1 opoc1.z 0˙=0.K
2 opoc1.u 1˙=1.K
3 opoc1.o ˙=ocK
4 1 2 3 opoc1 KOP˙1˙=0˙
5 eqid BaseK=BaseK
6 5 2 op1cl KOP1˙BaseK
7 5 1 op0cl KOP0˙BaseK
8 5 3 opcon1b KOP1˙BaseK0˙BaseK˙1˙=0˙˙0˙=1˙
9 6 7 8 mpd3an23 KOP˙1˙=0˙˙0˙=1˙
10 4 9 mpbid KOP˙0˙=1˙