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

Definition df-oposet 36194
Description: Define the class of orthoposets, which are bounded posets with an orthocomplementation operation. Note that (Base p ) e. dom ( lub 𝑝) 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 = {𝑝 ∈ Poset ∣ (((Base‘𝑝) ∈ dom (lub‘𝑝) ∧ (Base‘𝑝) ∈ dom (glb‘𝑝)) ∧ ∃𝑜(𝑜 = (oc‘𝑝) ∧ ∀𝑎 ∈ (Base‘𝑝)∀𝑏 ∈ (Base‘𝑝)(((𝑜𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜𝑏)(le‘𝑝)(𝑜𝑎))) ∧ (𝑎(join‘𝑝)(𝑜𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜𝑎)) = (0.‘𝑝))))}
Distinct variable group:   𝑎,𝑏,𝑝,𝑜

Detailed syntax breakdown of Definition df-oposet
StepHypRef Expression
1 cops 36190 . 2 class OP
2 vp . . . . . . . 8 setvar 𝑝
32cv 1527 . . . . . . 7 class 𝑝
4 cbs 16473 . . . . . . 7 class Base
53, 4cfv 6349 . . . . . 6 class (Base‘𝑝)
6 club 17542 . . . . . . . 8 class lub
73, 6cfv 6349 . . . . . . 7 class (lub‘𝑝)
87cdm 5549 . . . . . 6 class dom (lub‘𝑝)
95, 8wcel 2105 . . . . 5 wff (Base‘𝑝) ∈ dom (lub‘𝑝)
10 cglb 17543 . . . . . . . 8 class glb
113, 10cfv 6349 . . . . . . 7 class (glb‘𝑝)
1211cdm 5549 . . . . . 6 class dom (glb‘𝑝)
135, 12wcel 2105 . . . . 5 wff (Base‘𝑝) ∈ dom (glb‘𝑝)
149, 13wa 396 . . . 4 wff ((Base‘𝑝) ∈ dom (lub‘𝑝) ∧ (Base‘𝑝) ∈ dom (glb‘𝑝))
15 vo . . . . . . . 8 setvar 𝑜
1615cv 1527 . . . . . . 7 class 𝑜
17 coc 16563 . . . . . . . 8 class oc
183, 17cfv 6349 . . . . . . 7 class (oc‘𝑝)
1916, 18wceq 1528 . . . . . 6 wff 𝑜 = (oc‘𝑝)
20 va . . . . . . . . . . . . 13 setvar 𝑎
2120cv 1527 . . . . . . . . . . . 12 class 𝑎
2221, 16cfv 6349 . . . . . . . . . . 11 class (𝑜𝑎)
2322, 5wcel 2105 . . . . . . . . . 10 wff (𝑜𝑎) ∈ (Base‘𝑝)
2422, 16cfv 6349 . . . . . . . . . . 11 class (𝑜‘(𝑜𝑎))
2524, 21wceq 1528 . . . . . . . . . 10 wff (𝑜‘(𝑜𝑎)) = 𝑎
26 vb . . . . . . . . . . . . 13 setvar 𝑏
2726cv 1527 . . . . . . . . . . . 12 class 𝑏
28 cple 16562 . . . . . . . . . . . . 13 class le
293, 28cfv 6349 . . . . . . . . . . . 12 class (le‘𝑝)
3021, 27, 29wbr 5058 . . . . . . . . . . 11 wff 𝑎(le‘𝑝)𝑏
3127, 16cfv 6349 . . . . . . . . . . . 12 class (𝑜𝑏)
3231, 22, 29wbr 5058 . . . . . . . . . . 11 wff (𝑜𝑏)(le‘𝑝)(𝑜𝑎)
3330, 32wi 4 . . . . . . . . . 10 wff (𝑎(le‘𝑝)𝑏 → (𝑜𝑏)(le‘𝑝)(𝑜𝑎))
3423, 25, 33w3a 1079 . . . . . . . . 9 wff ((𝑜𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜𝑏)(le‘𝑝)(𝑜𝑎)))
35 cjn 17544 . . . . . . . . . . . 12 class join
363, 35cfv 6349 . . . . . . . . . . 11 class (join‘𝑝)
3721, 22, 36co 7145 . . . . . . . . . 10 class (𝑎(join‘𝑝)(𝑜𝑎))
38 cp1 17638 . . . . . . . . . . 11 class 1.
393, 38cfv 6349 . . . . . . . . . 10 class (1.‘𝑝)
4037, 39wceq 1528 . . . . . . . . 9 wff (𝑎(join‘𝑝)(𝑜𝑎)) = (1.‘𝑝)
41 cmee 17545 . . . . . . . . . . . 12 class meet
423, 41cfv 6349 . . . . . . . . . . 11 class (meet‘𝑝)
4321, 22, 42co 7145 . . . . . . . . . 10 class (𝑎(meet‘𝑝)(𝑜𝑎))
44 cp0 17637 . . . . . . . . . . 11 class 0.
453, 44cfv 6349 . . . . . . . . . 10 class (0.‘𝑝)
4643, 45wceq 1528 . . . . . . . . 9 wff (𝑎(meet‘𝑝)(𝑜𝑎)) = (0.‘𝑝)
4734, 40, 46w3a 1079 . . . . . . . 8 wff (((𝑜𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜𝑏)(le‘𝑝)(𝑜𝑎))) ∧ (𝑎(join‘𝑝)(𝑜𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜𝑎)) = (0.‘𝑝))
4847, 26, 5wral 3138 . . . . . . 7 wff 𝑏 ∈ (Base‘𝑝)(((𝑜𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜𝑏)(le‘𝑝)(𝑜𝑎))) ∧ (𝑎(join‘𝑝)(𝑜𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜𝑎)) = (0.‘𝑝))
4948, 20, 5wral 3138 . . . . . 6 wff 𝑎 ∈ (Base‘𝑝)∀𝑏 ∈ (Base‘𝑝)(((𝑜𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜𝑏)(le‘𝑝)(𝑜𝑎))) ∧ (𝑎(join‘𝑝)(𝑜𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜𝑎)) = (0.‘𝑝))
5019, 49wa 396 . . . . 5 wff (𝑜 = (oc‘𝑝) ∧ ∀𝑎 ∈ (Base‘𝑝)∀𝑏 ∈ (Base‘𝑝)(((𝑜𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜𝑏)(le‘𝑝)(𝑜𝑎))) ∧ (𝑎(join‘𝑝)(𝑜𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜𝑎)) = (0.‘𝑝)))
5150, 15wex 1771 . . . 4 wff 𝑜(𝑜 = (oc‘𝑝) ∧ ∀𝑎 ∈ (Base‘𝑝)∀𝑏 ∈ (Base‘𝑝)(((𝑜𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜𝑏)(le‘𝑝)(𝑜𝑎))) ∧ (𝑎(join‘𝑝)(𝑜𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜𝑎)) = (0.‘𝑝)))
5214, 51wa 396 . . 3 wff (((Base‘𝑝) ∈ dom (lub‘𝑝) ∧ (Base‘𝑝) ∈ dom (glb‘𝑝)) ∧ ∃𝑜(𝑜 = (oc‘𝑝) ∧ ∀𝑎 ∈ (Base‘𝑝)∀𝑏 ∈ (Base‘𝑝)(((𝑜𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜𝑏)(le‘𝑝)(𝑜𝑎))) ∧ (𝑎(join‘𝑝)(𝑜𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜𝑎)) = (0.‘𝑝))))
53 cpo 17540 . . 3 class Poset
5452, 2, 53crab 3142 . 2 class {𝑝 ∈ Poset ∣ (((Base‘𝑝) ∈ dom (lub‘𝑝) ∧ (Base‘𝑝) ∈ dom (glb‘𝑝)) ∧ ∃𝑜(𝑜 = (oc‘𝑝) ∧ ∀𝑎 ∈ (Base‘𝑝)∀𝑏 ∈ (Base‘𝑝)(((𝑜𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜𝑏)(le‘𝑝)(𝑜𝑎))) ∧ (𝑎(join‘𝑝)(𝑜𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜𝑎)) = (0.‘𝑝))))}
551, 54wceq 1528 1 wff OP = {𝑝 ∈ Poset ∣ (((Base‘𝑝) ∈ dom (lub‘𝑝) ∧ (Base‘𝑝) ∈ dom (glb‘𝑝)) ∧ ∃𝑜(𝑜 = (oc‘𝑝) ∧ ∀𝑎 ∈ (Base‘𝑝)∀𝑏 ∈ (Base‘𝑝)(((𝑜𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜𝑏)(le‘𝑝)(𝑜𝑎))) ∧ (𝑎(join‘𝑝)(𝑜𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜𝑎)) = (0.‘𝑝))))}
Colors of variables: wff setvar class
This definition is referenced by:  isopos  36198
  Copyright terms: Public domain W3C validator