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

Definition df-oposet 32813
 Description: Define the class of orthoposets, which are bounded posets with an orthocomplementation operation. Note that p ) e. dom ( lub means there is an upper bound , and similarly for the element. (Contributed by NM, 20-Oct-2011.) (Revised by NM, 13-Sep-2018.)
Assertion
Ref Expression
df-oposet
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-oposet
StepHypRef Expression
1 cops 32809 . 2
2 vp . . . . . . . 8
32cv 1451 . . . . . . 7
4 cbs 15199 . . . . . . 7
53, 4cfv 5589 . . . . . 6
6 club 16265 . . . . . . . 8
73, 6cfv 5589 . . . . . . 7
87cdm 4839 . . . . . 6
95, 8wcel 1904 . . . . 5
10 cglb 16266 . . . . . . . 8
113, 10cfv 5589 . . . . . . 7
1211cdm 4839 . . . . . 6
135, 12wcel 1904 . . . . 5
149, 13wa 376 . . . 4
15 vo . . . . . . . 8
1615cv 1451 . . . . . . 7
17 coc 15276 . . . . . . . 8
183, 17cfv 5589 . . . . . . 7
1916, 18wceq 1452 . . . . . 6
20 va . . . . . . . . . . . . 13
2120cv 1451 . . . . . . . . . . . 12
2221, 16cfv 5589 . . . . . . . . . . 11
2322, 5wcel 1904 . . . . . . . . . 10
2422, 16cfv 5589 . . . . . . . . . . 11
2524, 21wceq 1452 . . . . . . . . . 10
26 vb . . . . . . . . . . . . 13
2726cv 1451 . . . . . . . . . . . 12
28 cple 15275 . . . . . . . . . . . . 13
293, 28cfv 5589 . . . . . . . . . . . 12
3021, 27, 29wbr 4395 . . . . . . . . . . 11
3127, 16cfv 5589 . . . . . . . . . . . 12
3231, 22, 29wbr 4395 . . . . . . . . . . 11
3330, 32wi 4 . . . . . . . . . 10
3423, 25, 33w3a 1007 . . . . . . . . 9
35 cjn 16267 . . . . . . . . . . . 12
363, 35cfv 5589 . . . . . . . . . . 11
3721, 22, 36co 6308 . . . . . . . . . 10
38 cp1 16362 . . . . . . . . . . 11
393, 38cfv 5589 . . . . . . . . . 10
4037, 39wceq 1452 . . . . . . . . 9
41 cmee 16268 . . . . . . . . . . . 12
423, 41cfv 5589 . . . . . . . . . . 11
4321, 22, 42co 6308 . . . . . . . . . 10
44 cp0 16361 . . . . . . . . . . 11
453, 44cfv 5589 . . . . . . . . . 10
4643, 45wceq 1452 . . . . . . . . 9
4734, 40, 46w3a 1007 . . . . . . . 8
4847, 26, 5wral 2756 . . . . . . 7
4948, 20, 5wral 2756 . . . . . 6
5019, 49wa 376 . . . . 5
5150, 15wex 1671 . . . 4
5214, 51wa 376 . . 3
53 cpo 16263 . . 3
5452, 2, 53crab 2760 . 2
551, 54wceq 1452 1
 Colors of variables: wff setvar class This definition is referenced by:  isopos  32817
 Copyright terms: Public domain W3C validator