Metamath Proof Explorer


Theorem opoc1

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

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

Proof

Step Hyp Ref Expression
1 opoc1.z 0˙=0.K
2 opoc1.u 1˙=1.K
3 opoc1.o ˙=ocK
4 eqid BaseK=BaseK
5 4 1 op0cl KOP0˙BaseK
6 4 3 opoccl KOP0˙BaseK˙0˙BaseK
7 5 6 mpdan KOP˙0˙BaseK
8 eqid K=K
9 4 8 2 ople1 KOP˙0˙BaseK˙0˙K1˙
10 7 9 mpdan KOP˙0˙K1˙
11 4 2 op1cl KOP1˙BaseK
12 4 8 3 oplecon1b KOP1˙BaseK0˙BaseK˙1˙K0˙˙0˙K1˙
13 11 5 12 mpd3an23 KOP˙1˙K0˙˙0˙K1˙
14 10 13 mpbird KOP˙1˙K0˙
15 4 3 opoccl KOP1˙BaseK˙1˙BaseK
16 11 15 mpdan KOP˙1˙BaseK
17 4 8 1 ople0 KOP˙1˙BaseK˙1˙K0˙˙1˙=0˙
18 16 17 mpdan KOP˙1˙K0˙˙1˙=0˙
19 14 18 mpbid KOP˙1˙=0˙