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 33943
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 33939 . 2 class OP
2 vp . . . . . . . 8 setvar 𝑝
32cv 1479 . . . . . . 7 class 𝑝
4 cbs 15781 . . . . . . 7 class Base
53, 4cfv 5847 . . . . . 6 class (Base‘𝑝)
6 club 16863 . . . . . . . 8 class lub
73, 6cfv 5847 . . . . . . 7 class (lub‘𝑝)
87cdm 5074 . . . . . 6 class dom (lub‘𝑝)
95, 8wcel 1987 . . . . 5 wff (Base‘𝑝) ∈ dom (lub‘𝑝)
10 cglb 16864 . . . . . . . 8 class glb
113, 10cfv 5847 . . . . . . 7 class (glb‘𝑝)
1211cdm 5074 . . . . . 6 class dom (glb‘𝑝)
135, 12wcel 1987 . . . . 5 wff (Base‘𝑝) ∈ dom (glb‘𝑝)
149, 13wa 384 . . . 4 wff ((Base‘𝑝) ∈ dom (lub‘𝑝) ∧ (Base‘𝑝) ∈ dom (glb‘𝑝))
15 vo . . . . . . . 8 setvar 𝑜
1615cv 1479 . . . . . . 7 class 𝑜
17 coc 15870 . . . . . . . 8 class oc
183, 17cfv 5847 . . . . . . 7 class (oc‘𝑝)
1916, 18wceq 1480 . . . . . 6 wff 𝑜 = (oc‘𝑝)
20 va . . . . . . . . . . . . 13 setvar 𝑎
2120cv 1479 . . . . . . . . . . . 12 class 𝑎
2221, 16cfv 5847 . . . . . . . . . . 11 class (𝑜𝑎)
2322, 5wcel 1987 . . . . . . . . . 10 wff (𝑜𝑎) ∈ (Base‘𝑝)
2422, 16cfv 5847 . . . . . . . . . . 11 class (𝑜‘(𝑜𝑎))
2524, 21wceq 1480 . . . . . . . . . 10 wff (𝑜‘(𝑜𝑎)) = 𝑎
26 vb . . . . . . . . . . . . 13 setvar 𝑏
2726cv 1479 . . . . . . . . . . . 12 class 𝑏
28 cple 15869 . . . . . . . . . . . . 13 class le
293, 28cfv 5847 . . . . . . . . . . . 12 class (le‘𝑝)
3021, 27, 29wbr 4613 . . . . . . . . . . 11 wff 𝑎(le‘𝑝)𝑏
3127, 16cfv 5847 . . . . . . . . . . . 12 class (𝑜𝑏)
3231, 22, 29wbr 4613 . . . . . . . . . . 11 wff (𝑜𝑏)(le‘𝑝)(𝑜𝑎)
3330, 32wi 4 . . . . . . . . . 10 wff (𝑎(le‘𝑝)𝑏 → (𝑜𝑏)(le‘𝑝)(𝑜𝑎))
3423, 25, 33w3a 1036 . . . . . . . . 9 wff ((𝑜𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜𝑏)(le‘𝑝)(𝑜𝑎)))
35 cjn 16865 . . . . . . . . . . . 12 class join
363, 35cfv 5847 . . . . . . . . . . 11 class (join‘𝑝)
3721, 22, 36co 6604 . . . . . . . . . 10 class (𝑎(join‘𝑝)(𝑜𝑎))
38 cp1 16959 . . . . . . . . . . 11 class 1.
393, 38cfv 5847 . . . . . . . . . 10 class (1.‘𝑝)
4037, 39wceq 1480 . . . . . . . . 9 wff (𝑎(join‘𝑝)(𝑜𝑎)) = (1.‘𝑝)
41 cmee 16866 . . . . . . . . . . . 12 class meet
423, 41cfv 5847 . . . . . . . . . . 11 class (meet‘𝑝)
4321, 22, 42co 6604 . . . . . . . . . 10 class (𝑎(meet‘𝑝)(𝑜𝑎))
44 cp0 16958 . . . . . . . . . . 11 class 0.
453, 44cfv 5847 . . . . . . . . . 10 class (0.‘𝑝)
4643, 45wceq 1480 . . . . . . . . 9 wff (𝑎(meet‘𝑝)(𝑜𝑎)) = (0.‘𝑝)
4734, 40, 46w3a 1036 . . . . . . . 8 wff (((𝑜𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜𝑏)(le‘𝑝)(𝑜𝑎))) ∧ (𝑎(join‘𝑝)(𝑜𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜𝑎)) = (0.‘𝑝))
4847, 26, 5wral 2907 . . . . . . 7 wff 𝑏 ∈ (Base‘𝑝)(((𝑜𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜𝑏)(le‘𝑝)(𝑜𝑎))) ∧ (𝑎(join‘𝑝)(𝑜𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜𝑎)) = (0.‘𝑝))
4948, 20, 5wral 2907 . . . . . 6 wff 𝑎 ∈ (Base‘𝑝)∀𝑏 ∈ (Base‘𝑝)(((𝑜𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜𝑏)(le‘𝑝)(𝑜𝑎))) ∧ (𝑎(join‘𝑝)(𝑜𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜𝑎)) = (0.‘𝑝))
5019, 49wa 384 . . . . 5 wff (𝑜 = (oc‘𝑝) ∧ ∀𝑎 ∈ (Base‘𝑝)∀𝑏 ∈ (Base‘𝑝)(((𝑜𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜𝑏)(le‘𝑝)(𝑜𝑎))) ∧ (𝑎(join‘𝑝)(𝑜𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜𝑎)) = (0.‘𝑝)))
5150, 15wex 1701 . . . 4 wff 𝑜(𝑜 = (oc‘𝑝) ∧ ∀𝑎 ∈ (Base‘𝑝)∀𝑏 ∈ (Base‘𝑝)(((𝑜𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜𝑏)(le‘𝑝)(𝑜𝑎))) ∧ (𝑎(join‘𝑝)(𝑜𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜𝑎)) = (0.‘𝑝)))
5214, 51wa 384 . . 3 wff (((Base‘𝑝) ∈ dom (lub‘𝑝) ∧ (Base‘𝑝) ∈ dom (glb‘𝑝)) ∧ ∃𝑜(𝑜 = (oc‘𝑝) ∧ ∀𝑎 ∈ (Base‘𝑝)∀𝑏 ∈ (Base‘𝑝)(((𝑜𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜𝑏)(le‘𝑝)(𝑜𝑎))) ∧ (𝑎(join‘𝑝)(𝑜𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜𝑎)) = (0.‘𝑝))))
53 cpo 16861 . . 3 class Poset
5452, 2, 53crab 2911 . 2 class {𝑝 ∈ Poset ∣ (((Base‘𝑝) ∈ dom (lub‘𝑝) ∧ (Base‘𝑝) ∈ dom (glb‘𝑝)) ∧ ∃𝑜(𝑜 = (oc‘𝑝) ∧ ∀𝑎 ∈ (Base‘𝑝)∀𝑏 ∈ (Base‘𝑝)(((𝑜𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜𝑏)(le‘𝑝)(𝑜𝑎))) ∧ (𝑎(join‘𝑝)(𝑜𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜𝑎)) = (0.‘𝑝))))}
551, 54wceq 1480 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  33947
  Copyright terms: Public domain W3C validator