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

Definition df-oposet 29988
Description: Define the class of orthoposets. (Contributed by NM, 20-Oct-2011.)
Assertion
Ref Expression
df-oposet  |-  OP  =  { p  e.  Poset  |  ( ( ( 0. `  p )  e.  (
Base `  p )  /\  ( 1. `  p
)  e.  ( Base `  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 29984 . 2  class  OP
2 vp . . . . . . . 8  set  p
32cv 1631 . . . . . . 7  class  p
4 cp0 14159 . . . . . . 7  class  0.
53, 4cfv 5271 . . . . . 6  class  ( 0.
`  p )
6 cbs 13164 . . . . . . 7  class  Base
73, 6cfv 5271 . . . . . 6  class  ( Base `  p )
85, 7wcel 1696 . . . . 5  wff  ( 0.
`  p )  e.  ( Base `  p
)
9 cp1 14160 . . . . . . 7  class  1.
103, 9cfv 5271 . . . . . 6  class  ( 1.
`  p )
1110, 7wcel 1696 . . . . 5  wff  ( 1.
`  p )  e.  ( Base `  p
)
128, 11wa 358 . . . 4  wff  ( ( 0. `  p )  e.  ( Base `  p
)  /\  ( 1. `  p )  e.  (
Base `  p )
)
13 vo . . . . . . . 8  set  o
1413cv 1631 . . . . . . 7  class  o
15 coc 13232 . . . . . . . 8  class  oc
163, 15cfv 5271 . . . . . . 7  class  ( oc
`  p )
1714, 16wceq 1632 . . . . . 6  wff  o  =  ( oc `  p
)
18 va . . . . . . . . . . . . 13  set  a
1918cv 1631 . . . . . . . . . . . 12  class  a
2019, 14cfv 5271 . . . . . . . . . . 11  class  ( o `
 a )
2120, 7wcel 1696 . . . . . . . . . 10  wff  ( o `
 a )  e.  ( Base `  p
)
2220, 14cfv 5271 . . . . . . . . . . 11  class  ( o `
 ( o `  a ) )
2322, 19wceq 1632 . . . . . . . . . 10  wff  ( o `
 ( o `  a ) )  =  a
24 vb . . . . . . . . . . . . 13  set  b
2524cv 1631 . . . . . . . . . . . 12  class  b
26 cple 13231 . . . . . . . . . . . . 13  class  le
273, 26cfv 5271 . . . . . . . . . . . 12  class  ( le
`  p )
2819, 25, 27wbr 4039 . . . . . . . . . . 11  wff  a ( le `  p ) b
2925, 14cfv 5271 . . . . . . . . . . . 12  class  ( o `
 b )
3029, 20, 27wbr 4039 . . . . . . . . . . 11  wff  ( o `
 b ) ( le `  p ) ( o `  a
)
3128, 30wi 4 . . . . . . . . . 10  wff  ( a ( le `  p
) b  ->  (
o `  b )
( le `  p
) ( o `  a ) )
3221, 23, 31w3a 934 . . . . . . . . 9  wff  ( ( o `  a )  e.  ( Base `  p
)  /\  ( o `  ( o `  a
) )  =  a  /\  ( a ( le `  p ) b  ->  ( o `  b ) ( le
`  p ) ( o `  a ) ) )
33 cjn 14094 . . . . . . . . . . . 12  class  join
343, 33cfv 5271 . . . . . . . . . . 11  class  ( join `  p )
3519, 20, 34co 5874 . . . . . . . . . 10  class  ( a ( join `  p
) ( o `  a ) )
3635, 10wceq 1632 . . . . . . . . 9  wff  ( a ( join `  p
) ( o `  a ) )  =  ( 1. `  p
)
37 cmee 14095 . . . . . . . . . . . 12  class  meet
383, 37cfv 5271 . . . . . . . . . . 11  class  ( meet `  p )
3919, 20, 38co 5874 . . . . . . . . . 10  class  ( a ( meet `  p
) ( o `  a ) )
4039, 5wceq 1632 . . . . . . . . 9  wff  ( a ( meet `  p
) ( o `  a ) )  =  ( 0. `  p
)
4132, 36, 40w3a 934 . . . . . . . 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 ) )
4241, 24, 7wral 2556 . . . . . . 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 ) )
4342, 18, 7wral 2556 . . . . . 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 ) )
4417, 43wa 358 . . . . 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 ) ) )
4544, 13wex 1531 . . . 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 ) ) )
4612, 45wa 358 . . 3  wff  ( ( ( 0. `  p
)  e.  ( Base `  p )  /\  ( 1. `  p )  e.  ( Base `  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 ) ) ) )
47 cpo 14090 . . 3  class  Poset
4846, 2, 47crab 2560 . 2  class  { p  e.  Poset  |  ( ( ( 0. `  p
)  e.  ( Base `  p )  /\  ( 1. `  p )  e.  ( Base `  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 ) ) ) ) }
491, 48wceq 1632 1  wff  OP  =  { p  e.  Poset  |  ( ( ( 0. `  p )  e.  (
Base `  p )  /\  ( 1. `  p
)  e.  ( Base `  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 set class
This definition is referenced by:  isopos  29992
  Copyright terms: Public domain W3C validator