Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-oposet Structured version   Unicode version

Definition df-oposet 32175
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.)
Assertion
Ref Expression
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 ) ) ) ) }
Distinct variable group:    a, b, p, o

Detailed syntax breakdown of Definition df-oposet
StepHypRef Expression
1 cops 32171 . 2  class  OP
2 vp . . . . . . . 8  setvar  p
32cv 1404 . . . . . . 7  class  p
4 cbs 14733 . . . . . . 7  class  Base
53, 4cfv 5525 . . . . . 6  class  ( Base `  p )
6 club 15787 . . . . . . . 8  class  lub
73, 6cfv 5525 . . . . . . 7  class  ( lub `  p )
87cdm 4942 . . . . . 6  class  dom  ( lub `  p )
95, 8wcel 1842 . . . . 5  wff  ( Base `  p )  e.  dom  ( lub `  p )
10 cglb 15788 . . . . . . . 8  class  glb
113, 10cfv 5525 . . . . . . 7  class  ( glb `  p )
1211cdm 4942 . . . . . 6  class  dom  ( glb `  p )
135, 12wcel 1842 . . . . 5  wff  ( Base `  p )  e.  dom  ( glb `  p )
149, 13wa 367 . . . 4  wff  ( (
Base `  p )  e.  dom  ( lub `  p
)  /\  ( Base `  p )  e.  dom  ( glb `  p ) )
15 vo . . . . . . . 8  setvar  o
1615cv 1404 . . . . . . 7  class  o
17 coc 14809 . . . . . . . 8  class  oc
183, 17cfv 5525 . . . . . . 7  class  ( oc
`  p )
1916, 18wceq 1405 . . . . . 6  wff  o  =  ( oc `  p
)
20 va . . . . . . . . . . . . 13  setvar  a
2120cv 1404 . . . . . . . . . . . 12  class  a
2221, 16cfv 5525 . . . . . . . . . . 11  class  ( o `
 a )
2322, 5wcel 1842 . . . . . . . . . 10  wff  ( o `
 a )  e.  ( Base `  p
)
2422, 16cfv 5525 . . . . . . . . . . 11  class  ( o `
 ( o `  a ) )
2524, 21wceq 1405 . . . . . . . . . 10  wff  ( o `
 ( o `  a ) )  =  a
26 vb . . . . . . . . . . . . 13  setvar  b
2726cv 1404 . . . . . . . . . . . 12  class  b
28 cple 14808 . . . . . . . . . . . . 13  class  le
293, 28cfv 5525 . . . . . . . . . . . 12  class  ( le
`  p )
3021, 27, 29wbr 4394 . . . . . . . . . . 11  wff  a ( le `  p ) b
3127, 16cfv 5525 . . . . . . . . . . . 12  class  ( o `
 b )
3231, 22, 29wbr 4394 . . . . . . . . . . 11  wff  ( o `
 b ) ( le `  p ) ( o `  a
)
3330, 32wi 4 . . . . . . . . . 10  wff  ( a ( le `  p
) b  ->  (
o `  b )
( le `  p
) ( o `  a ) )
3423, 25, 33w3a 974 . . . . . . . . 9  wff  ( ( o `  a )  e.  ( Base `  p
)  /\  ( o `  ( o `  a
) )  =  a  /\  ( a ( le `  p ) b  ->  ( o `  b ) ( le
`  p ) ( o `  a ) ) )
35 cjn 15789 . . . . . . . . . . . 12  class  join
363, 35cfv 5525 . . . . . . . . . . 11  class  ( join `  p )
3721, 22, 36co 6234 . . . . . . . . . 10  class  ( a ( join `  p
) ( o `  a ) )
38 cp1 15884 . . . . . . . . . . 11  class  1.
393, 38cfv 5525 . . . . . . . . . 10  class  ( 1.
`  p )
4037, 39wceq 1405 . . . . . . . . 9  wff  ( a ( join `  p
) ( o `  a ) )  =  ( 1. `  p
)
41 cmee 15790 . . . . . . . . . . . 12  class  meet
423, 41cfv 5525 . . . . . . . . . . 11  class  ( meet `  p )
4321, 22, 42co 6234 . . . . . . . . . 10  class  ( a ( meet `  p
) ( o `  a ) )
44 cp0 15883 . . . . . . . . . . 11  class  0.
453, 44cfv 5525 . . . . . . . . . 10  class  ( 0.
`  p )
4643, 45wceq 1405 . . . . . . . . 9  wff  ( a ( meet `  p
) ( o `  a ) )  =  ( 0. `  p
)
4734, 40, 46w3a 974 . . . . . . . 8  wff  ( ( ( 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 ) )
4847, 26, 5wral 2753 . . . . . . 7  wff  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 ) )
4948, 20, 5wral 2753 . . . . . 6  wff  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 ) )
5019, 49wa 367 . . . . 5  wff  ( 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 ) ) )
5150, 15wex 1633 . . . 4  wff  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 ) ) )
5214, 51wa 367 . . 3  wff  ( ( ( 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 cpo 15785 . . 3  class  Poset
5452, 2, 53crab 2757 . 2  class  { 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 ) ) ) ) }
551, 54wceq 1405 1  wff  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 ) ) ) ) }
Colors of variables: wff setvar class
This definition is referenced by:  isopos  32179
  Copyright terms: Public domain W3C validator