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 ) ) ) ) }