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 32705
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 32701 . 2  class  OP
2 vp . . . . . . . 8  setvar  p
32cv 1437 . . . . . . 7  class  p
4 cbs 15114 . . . . . . 7  class  Base
53, 4cfv 5599 . . . . . 6  class  ( Base `  p )
6 club 16180 . . . . . . . 8  class  lub
73, 6cfv 5599 . . . . . . 7  class  ( lub `  p )
87cdm 4851 . . . . . 6  class  dom  ( lub `  p )
95, 8wcel 1869 . . . . 5  wff  ( Base `  p )  e.  dom  ( lub `  p )
10 cglb 16181 . . . . . . . 8  class  glb
113, 10cfv 5599 . . . . . . 7  class  ( glb `  p )
1211cdm 4851 . . . . . 6  class  dom  ( glb `  p )
135, 12wcel 1869 . . . . 5  wff  ( Base `  p )  e.  dom  ( glb `  p )
149, 13wa 371 . . . 4  wff  ( (
Base `  p )  e.  dom  ( lub `  p
)  /\  ( Base `  p )  e.  dom  ( glb `  p ) )
15 vo . . . . . . . 8  setvar  o
1615cv 1437 . . . . . . 7  class  o
17 coc 15191 . . . . . . . 8  class  oc
183, 17cfv 5599 . . . . . . 7  class  ( oc
`  p )
1916, 18wceq 1438 . . . . . 6  wff  o  =  ( oc `  p
)
20 va . . . . . . . . . . . . 13  setvar  a
2120cv 1437 . . . . . . . . . . . 12  class  a
2221, 16cfv 5599 . . . . . . . . . . 11  class  ( o `
 a )
2322, 5wcel 1869 . . . . . . . . . 10  wff  ( o `
 a )  e.  ( Base `  p
)
2422, 16cfv 5599 . . . . . . . . . . 11  class  ( o `
 ( o `  a ) )
2524, 21wceq 1438 . . . . . . . . . 10  wff  ( o `
 ( o `  a ) )  =  a
26 vb . . . . . . . . . . . . 13  setvar  b
2726cv 1437 . . . . . . . . . . . 12  class  b
28 cple 15190 . . . . . . . . . . . . 13  class  le
293, 28cfv 5599 . . . . . . . . . . . 12  class  ( le
`  p )
3021, 27, 29wbr 4421 . . . . . . . . . . 11  wff  a ( le `  p ) b
3127, 16cfv 5599 . . . . . . . . . . . 12  class  ( o `
 b )
3231, 22, 29wbr 4421 . . . . . . . . . . 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 983 . . . . . . . . 9  wff  ( ( o `  a )  e.  ( Base `  p
)  /\  ( o `  ( o `  a
) )  =  a  /\  ( a ( le `  p ) b  ->  ( o `  b ) ( le
`  p ) ( o `  a ) ) )
35 cjn 16182 . . . . . . . . . . . 12  class  join
363, 35cfv 5599 . . . . . . . . . . 11  class  ( join `  p )
3721, 22, 36co 6303 . . . . . . . . . 10  class  ( a ( join `  p
) ( o `  a ) )
38 cp1 16277 . . . . . . . . . . 11  class  1.
393, 38cfv 5599 . . . . . . . . . 10  class  ( 1.
`  p )
4037, 39wceq 1438 . . . . . . . . 9  wff  ( a ( join `  p
) ( o `  a ) )  =  ( 1. `  p
)
41 cmee 16183 . . . . . . . . . . . 12  class  meet
423, 41cfv 5599 . . . . . . . . . . 11  class  ( meet `  p )
4321, 22, 42co 6303 . . . . . . . . . 10  class  ( a ( meet `  p
) ( o `  a ) )
44 cp0 16276 . . . . . . . . . . 11  class  0.
453, 44cfv 5599 . . . . . . . . . 10  class  ( 0.
`  p )
4643, 45wceq 1438 . . . . . . . . 9  wff  ( a ( meet `  p
) ( o `  a ) )  =  ( 0. `  p
)
4734, 40, 46w3a 983 . . . . . . . 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 2776 . . . . . . 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 2776 . . . . . 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 371 . . . . 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 1660 . . . 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 371 . . 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 16178 . . 3  class  Poset
5452, 2, 53crab 2780 . 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 1438 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  32709
  Copyright terms: Public domain W3C validator