# Metamath Proof Explorer

## Definition df-oposet

Description: Define the class of orthoposets, which are bounded posets with an orthocomplementation operation. Note that ( Base p ) e. dom ( lub p ) means there is an upper bound 1. , and similarly for the 0. element. (Contributed by NM, 20-Oct-2011) (Revised by NM, 13-Sep-2018)

Ref Expression
Assertion df-oposet ${⊢}\mathrm{OP}=\left\{{p}\in \mathrm{Poset}|\left(\left({\mathrm{Base}}_{{p}}\in \mathrm{dom}\mathrm{lub}\left({p}\right)\wedge {\mathrm{Base}}_{{p}}\in \mathrm{dom}\mathrm{glb}\left({p}\right)\right)\wedge \exists {o}\phantom{\rule{.4em}{0ex}}\left({o}=\mathrm{oc}\left({p}\right)\wedge \forall {a}\in {\mathrm{Base}}_{{p}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{p}}\phantom{\rule{.4em}{0ex}}\left(\left({o}\left({a}\right)\in {\mathrm{Base}}_{{p}}\wedge {o}\left({o}\left({a}\right)\right)={a}\wedge \left({a}{\le }_{{p}}{b}\to {o}\left({b}\right){\le }_{{p}}{o}\left({a}\right)\right)\right)\wedge {a}\mathrm{join}\left({p}\right){o}\left({a}\right)=\mathrm{1.}\left({p}\right)\wedge {a}\mathrm{meet}\left({p}\right){o}\left({a}\right)=\mathrm{0.}\left({p}\right)\right)\right)\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cops ${class}\mathrm{OP}$
1 vp ${setvar}{p}$
2 cpo ${class}\mathrm{Poset}$
3 cbs ${class}\mathrm{Base}$
4 1 cv ${setvar}{p}$
5 4 3 cfv ${class}{\mathrm{Base}}_{{p}}$
6 club ${class}\mathrm{lub}$
7 4 6 cfv ${class}\mathrm{lub}\left({p}\right)$
8 7 cdm ${class}\mathrm{dom}\mathrm{lub}\left({p}\right)$
9 5 8 wcel ${wff}{\mathrm{Base}}_{{p}}\in \mathrm{dom}\mathrm{lub}\left({p}\right)$
10 cglb ${class}\mathrm{glb}$
11 4 10 cfv ${class}\mathrm{glb}\left({p}\right)$
12 11 cdm ${class}\mathrm{dom}\mathrm{glb}\left({p}\right)$
13 5 12 wcel ${wff}{\mathrm{Base}}_{{p}}\in \mathrm{dom}\mathrm{glb}\left({p}\right)$
14 9 13 wa ${wff}\left({\mathrm{Base}}_{{p}}\in \mathrm{dom}\mathrm{lub}\left({p}\right)\wedge {\mathrm{Base}}_{{p}}\in \mathrm{dom}\mathrm{glb}\left({p}\right)\right)$
15 vo ${setvar}{o}$
16 15 cv ${setvar}{o}$
17 coc ${class}\mathrm{oc}$
18 4 17 cfv ${class}\mathrm{oc}\left({p}\right)$
19 16 18 wceq ${wff}{o}=\mathrm{oc}\left({p}\right)$
20 va ${setvar}{a}$
21 vb ${setvar}{b}$
22 20 cv ${setvar}{a}$
23 22 16 cfv ${class}{o}\left({a}\right)$
24 23 5 wcel ${wff}{o}\left({a}\right)\in {\mathrm{Base}}_{{p}}$
25 23 16 cfv ${class}{o}\left({o}\left({a}\right)\right)$
26 25 22 wceq ${wff}{o}\left({o}\left({a}\right)\right)={a}$
27 cple ${class}\mathrm{le}$
28 4 27 cfv ${class}{\le }_{{p}}$
29 21 cv ${setvar}{b}$
30 22 29 28 wbr ${wff}{a}{\le }_{{p}}{b}$
31 29 16 cfv ${class}{o}\left({b}\right)$
32 31 23 28 wbr ${wff}{o}\left({b}\right){\le }_{{p}}{o}\left({a}\right)$
33 30 32 wi ${wff}\left({a}{\le }_{{p}}{b}\to {o}\left({b}\right){\le }_{{p}}{o}\left({a}\right)\right)$
34 24 26 33 w3a ${wff}\left({o}\left({a}\right)\in {\mathrm{Base}}_{{p}}\wedge {o}\left({o}\left({a}\right)\right)={a}\wedge \left({a}{\le }_{{p}}{b}\to {o}\left({b}\right){\le }_{{p}}{o}\left({a}\right)\right)\right)$
35 cjn ${class}\mathrm{join}$
36 4 35 cfv ${class}\mathrm{join}\left({p}\right)$
37 22 23 36 co ${class}\left({a}\mathrm{join}\left({p}\right){o}\left({a}\right)\right)$
38 cp1 ${class}\mathrm{1.}$
39 4 38 cfv ${class}\mathrm{1.}\left({p}\right)$
40 37 39 wceq ${wff}{a}\mathrm{join}\left({p}\right){o}\left({a}\right)=\mathrm{1.}\left({p}\right)$
41 cmee ${class}\mathrm{meet}$
42 4 41 cfv ${class}\mathrm{meet}\left({p}\right)$
43 22 23 42 co ${class}\left({a}\mathrm{meet}\left({p}\right){o}\left({a}\right)\right)$
44 cp0 ${class}\mathrm{0.}$
45 4 44 cfv ${class}\mathrm{0.}\left({p}\right)$
46 43 45 wceq ${wff}{a}\mathrm{meet}\left({p}\right){o}\left({a}\right)=\mathrm{0.}\left({p}\right)$
47 34 40 46 w3a ${wff}\left(\left({o}\left({a}\right)\in {\mathrm{Base}}_{{p}}\wedge {o}\left({o}\left({a}\right)\right)={a}\wedge \left({a}{\le }_{{p}}{b}\to {o}\left({b}\right){\le }_{{p}}{o}\left({a}\right)\right)\right)\wedge {a}\mathrm{join}\left({p}\right){o}\left({a}\right)=\mathrm{1.}\left({p}\right)\wedge {a}\mathrm{meet}\left({p}\right){o}\left({a}\right)=\mathrm{0.}\left({p}\right)\right)$
48 47 21 5 wral ${wff}\forall {b}\in {\mathrm{Base}}_{{p}}\phantom{\rule{.4em}{0ex}}\left(\left({o}\left({a}\right)\in {\mathrm{Base}}_{{p}}\wedge {o}\left({o}\left({a}\right)\right)={a}\wedge \left({a}{\le }_{{p}}{b}\to {o}\left({b}\right){\le }_{{p}}{o}\left({a}\right)\right)\right)\wedge {a}\mathrm{join}\left({p}\right){o}\left({a}\right)=\mathrm{1.}\left({p}\right)\wedge {a}\mathrm{meet}\left({p}\right){o}\left({a}\right)=\mathrm{0.}\left({p}\right)\right)$
49 48 20 5 wral ${wff}\forall {a}\in {\mathrm{Base}}_{{p}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{p}}\phantom{\rule{.4em}{0ex}}\left(\left({o}\left({a}\right)\in {\mathrm{Base}}_{{p}}\wedge {o}\left({o}\left({a}\right)\right)={a}\wedge \left({a}{\le }_{{p}}{b}\to {o}\left({b}\right){\le }_{{p}}{o}\left({a}\right)\right)\right)\wedge {a}\mathrm{join}\left({p}\right){o}\left({a}\right)=\mathrm{1.}\left({p}\right)\wedge {a}\mathrm{meet}\left({p}\right){o}\left({a}\right)=\mathrm{0.}\left({p}\right)\right)$
50 19 49 wa ${wff}\left({o}=\mathrm{oc}\left({p}\right)\wedge \forall {a}\in {\mathrm{Base}}_{{p}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{p}}\phantom{\rule{.4em}{0ex}}\left(\left({o}\left({a}\right)\in {\mathrm{Base}}_{{p}}\wedge {o}\left({o}\left({a}\right)\right)={a}\wedge \left({a}{\le }_{{p}}{b}\to {o}\left({b}\right){\le }_{{p}}{o}\left({a}\right)\right)\right)\wedge {a}\mathrm{join}\left({p}\right){o}\left({a}\right)=\mathrm{1.}\left({p}\right)\wedge {a}\mathrm{meet}\left({p}\right){o}\left({a}\right)=\mathrm{0.}\left({p}\right)\right)\right)$
51 50 15 wex ${wff}\exists {o}\phantom{\rule{.4em}{0ex}}\left({o}=\mathrm{oc}\left({p}\right)\wedge \forall {a}\in {\mathrm{Base}}_{{p}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{p}}\phantom{\rule{.4em}{0ex}}\left(\left({o}\left({a}\right)\in {\mathrm{Base}}_{{p}}\wedge {o}\left({o}\left({a}\right)\right)={a}\wedge \left({a}{\le }_{{p}}{b}\to {o}\left({b}\right){\le }_{{p}}{o}\left({a}\right)\right)\right)\wedge {a}\mathrm{join}\left({p}\right){o}\left({a}\right)=\mathrm{1.}\left({p}\right)\wedge {a}\mathrm{meet}\left({p}\right){o}\left({a}\right)=\mathrm{0.}\left({p}\right)\right)\right)$
52 14 51 wa ${wff}\left(\left({\mathrm{Base}}_{{p}}\in \mathrm{dom}\mathrm{lub}\left({p}\right)\wedge {\mathrm{Base}}_{{p}}\in \mathrm{dom}\mathrm{glb}\left({p}\right)\right)\wedge \exists {o}\phantom{\rule{.4em}{0ex}}\left({o}=\mathrm{oc}\left({p}\right)\wedge \forall {a}\in {\mathrm{Base}}_{{p}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{p}}\phantom{\rule{.4em}{0ex}}\left(\left({o}\left({a}\right)\in {\mathrm{Base}}_{{p}}\wedge {o}\left({o}\left({a}\right)\right)={a}\wedge \left({a}{\le }_{{p}}{b}\to {o}\left({b}\right){\le }_{{p}}{o}\left({a}\right)\right)\right)\wedge {a}\mathrm{join}\left({p}\right){o}\left({a}\right)=\mathrm{1.}\left({p}\right)\wedge {a}\mathrm{meet}\left({p}\right){o}\left({a}\right)=\mathrm{0.}\left({p}\right)\right)\right)\right)$
53 52 1 2 crab ${class}\left\{{p}\in \mathrm{Poset}|\left(\left({\mathrm{Base}}_{{p}}\in \mathrm{dom}\mathrm{lub}\left({p}\right)\wedge {\mathrm{Base}}_{{p}}\in \mathrm{dom}\mathrm{glb}\left({p}\right)\right)\wedge \exists {o}\phantom{\rule{.4em}{0ex}}\left({o}=\mathrm{oc}\left({p}\right)\wedge \forall {a}\in {\mathrm{Base}}_{{p}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{p}}\phantom{\rule{.4em}{0ex}}\left(\left({o}\left({a}\right)\in {\mathrm{Base}}_{{p}}\wedge {o}\left({o}\left({a}\right)\right)={a}\wedge \left({a}{\le }_{{p}}{b}\to {o}\left({b}\right){\le }_{{p}}{o}\left({a}\right)\right)\right)\wedge {a}\mathrm{join}\left({p}\right){o}\left({a}\right)=\mathrm{1.}\left({p}\right)\wedge {a}\mathrm{meet}\left({p}\right){o}\left({a}\right)=\mathrm{0.}\left({p}\right)\right)\right)\right)\right\}$
54 0 53 wceq ${wff}\mathrm{OP}=\left\{{p}\in \mathrm{Poset}|\left(\left({\mathrm{Base}}_{{p}}\in \mathrm{dom}\mathrm{lub}\left({p}\right)\wedge {\mathrm{Base}}_{{p}}\in \mathrm{dom}\mathrm{glb}\left({p}\right)\right)\wedge \exists {o}\phantom{\rule{.4em}{0ex}}\left({o}=\mathrm{oc}\left({p}\right)\wedge \forall {a}\in {\mathrm{Base}}_{{p}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{p}}\phantom{\rule{.4em}{0ex}}\left(\left({o}\left({a}\right)\in {\mathrm{Base}}_{{p}}\wedge {o}\left({o}\left({a}\right)\right)={a}\wedge \left({a}{\le }_{{p}}{b}\to {o}\left({b}\right){\le }_{{p}}{o}\left({a}\right)\right)\right)\wedge {a}\mathrm{join}\left({p}\right){o}\left({a}\right)=\mathrm{1.}\left({p}\right)\wedge {a}\mathrm{meet}\left({p}\right){o}\left({a}\right)=\mathrm{0.}\left({p}\right)\right)\right)\right)\right\}$