# 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
`|- OP = { p e. Poset | ( ( ( Base ` p ) e. dom ( lub ` p ) /\ ( Base ` p ) e. dom ( glb ` p ) ) /\ E. o ( o = ( oc ` p ) /\ A. a e. ( Base ` p ) A. b e. ( Base ` p ) ( ( ( o ` a ) e. ( Base ` p ) /\ ( o ` ( o ` a ) ) = a /\ ( a ( le ` p ) b -> ( o ` b ) ( le ` p ) ( o ` a ) ) ) /\ ( a ( join ` p ) ( o ` a ) ) = ( 1. ` p ) /\ ( a ( meet ` p ) ( o ` a ) ) = ( 0. ` p ) ) ) ) }`

### Detailed syntax breakdown

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