Description: Orthocomplement of orthoposet zero. (Contributed by NM, 24-Jan-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | opoc1.z | |
|
opoc1.u | |
||
opoc1.o | |
||
Assertion | opoc0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opoc1.z | |
|
2 | opoc1.u | |
|
3 | opoc1.o | |
|
4 | 1 2 3 | opoc1 | |
5 | eqid | |
|
6 | 5 2 | op1cl | |
7 | 5 1 | op0cl | |
8 | 5 3 | opcon1b | |
9 | 6 7 8 | mpd3an23 | |
10 | 4 9 | mpbid | |