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 34379
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 34375 . 2  class  OP
2 vp . . . . . . . 8  setvar  p
32cv 1378 . . . . . . 7  class  p
4 cbs 14506 . . . . . . 7  class  Base
53, 4cfv 5594 . . . . . 6  class  ( Base `  p )
6 club 15445 . . . . . . . 8  class  lub
73, 6cfv 5594 . . . . . . 7  class  ( lub `  p )
87cdm 5005 . . . . . 6  class  dom  ( lub `  p )
95, 8wcel 1767 . . . . 5  wff  ( Base `  p )  e.  dom  ( lub `  p )
10 cglb 15446 . . . . . . . 8  class  glb
113, 10cfv 5594 . . . . . . 7  class  ( glb `  p )
1211cdm 5005 . . . . . 6  class  dom  ( glb `  p )
135, 12wcel 1767 . . . . 5  wff  ( Base `  p )  e.  dom  ( glb `  p )
149, 13wa 369 . . . 4  wff  ( (
Base `  p )  e.  dom  ( lub `  p
)  /\  ( Base `  p )  e.  dom  ( glb `  p ) )
15 vo . . . . . . . 8  setvar  o
1615cv 1378 . . . . . . 7  class  o
17 coc 14579 . . . . . . . 8  class  oc
183, 17cfv 5594 . . . . . . 7  class  ( oc
`  p )
1916, 18wceq 1379 . . . . . 6  wff  o  =  ( oc `  p
)
20 va . . . . . . . . . . . . 13  setvar  a
2120cv 1378 . . . . . . . . . . . 12  class  a
2221, 16cfv 5594 . . . . . . . . . . 11  class  ( o `
 a )
2322, 5wcel 1767 . . . . . . . . . 10  wff  ( o `
 a )  e.  ( Base `  p
)
2422, 16cfv 5594 . . . . . . . . . . 11  class  ( o `
 ( o `  a ) )
2524, 21wceq 1379 . . . . . . . . . 10  wff  ( o `
 ( o `  a ) )  =  a
26 vb . . . . . . . . . . . . 13  setvar  b
2726cv 1378 . . . . . . . . . . . 12  class  b
28 cple 14578 . . . . . . . . . . . . 13  class  le
293, 28cfv 5594 . . . . . . . . . . . 12  class  ( le
`  p )
3021, 27, 29wbr 4453 . . . . . . . . . . 11  wff  a ( le `  p ) b
3127, 16cfv 5594 . . . . . . . . . . . 12  class  ( o `
 b )
3231, 22, 29wbr 4453 . . . . . . . . . . 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 973 . . . . . . . . 9  wff  ( ( o `  a )  e.  ( Base `  p
)  /\  ( o `  ( o `  a
) )  =  a  /\  ( a ( le `  p ) b  ->  ( o `  b ) ( le
`  p ) ( o `  a ) ) )
35 cjn 15447 . . . . . . . . . . . 12  class  join
363, 35cfv 5594 . . . . . . . . . . 11  class  ( join `  p )
3721, 22, 36co 6295 . . . . . . . . . 10  class  ( a ( join `  p
) ( o `  a ) )
38 cp1 15541 . . . . . . . . . . 11  class  1.
393, 38cfv 5594 . . . . . . . . . 10  class  ( 1.
`  p )
4037, 39wceq 1379 . . . . . . . . 9  wff  ( a ( join `  p
) ( o `  a ) )  =  ( 1. `  p
)
41 cmee 15448 . . . . . . . . . . . 12  class  meet
423, 41cfv 5594 . . . . . . . . . . 11  class  ( meet `  p )
4321, 22, 42co 6295 . . . . . . . . . 10  class  ( a ( meet `  p
) ( o `  a ) )
44 cp0 15540 . . . . . . . . . . 11  class  0.
453, 44cfv 5594 . . . . . . . . . 10  class  ( 0.
`  p )
4643, 45wceq 1379 . . . . . . . . 9  wff  ( a ( meet `  p
) ( o `  a ) )  =  ( 0. `  p
)
4734, 40, 46w3a 973 . . . . . . . 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 2817 . . . . . . 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 2817 . . . . . 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 369 . . . . 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 1596 . . . 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 369 . . 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 15443 . . 3  class  Poset
5452, 2, 53crab 2821 . 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 1379 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  34383
  Copyright terms: Public domain W3C validator