Definition df-oposet 39177

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

Step	Hyp	Ref	Expression
1		cops 39173	. 2 class OP
2		vp	. . . . . . . 8 setvar 𝑝
3	2	cv 1539	. . . . . . 7 class 𝑝
4		cbs 17247	. . . . . . 7 class Base
5	3, 4	cfv 6561	. . . . . 6 class (Base‘𝑝)
6		club 18355	. . . . . . . 8 class lub
7	3, 6	cfv 6561	. . . . . . 7 class (lub‘𝑝)
8	7	cdm 5685	. . . . . 6 class dom (lub‘𝑝)
9	5, 8	wcel 2108	. . . . 5 wff (Base‘𝑝) ∈ dom (lub‘𝑝)
10		cglb 18356	. . . . . . . 8 class glb
11	3, 10	cfv 6561	. . . . . . 7 class (glb‘𝑝)
12	11	cdm 5685	. . . . . 6 class dom (glb‘𝑝)
13	5, 12	wcel 2108	. . . . 5 wff (Base‘𝑝) ∈ dom (glb‘𝑝)
14	9, 13	wa 395	. . . 4 wff ((Base‘𝑝) ∈ dom (lub‘𝑝) ∧ (Base‘𝑝) ∈ dom (glb‘𝑝))
15		vo	. . . . . . . 8 setvar 𝑜
16	15	cv 1539	. . . . . . 7 class 𝑜
17		coc 17305	. . . . . . . 8 class oc
18	3, 17	cfv 6561	. . . . . . 7 class (oc‘𝑝)
19	16, 18	wceq 1540	. . . . . 6 wff 𝑜 = (oc‘𝑝)
20		va	. . . . . . . . . . . . 13 setvar 𝑎
21	20	cv 1539	. . . . . . . . . . . 12 class 𝑎
22	21, 16	cfv 6561	. . . . . . . . . . 11 class (𝑜‘𝑎)
23	22, 5	wcel 2108	. . . . . . . . . 10 wff (𝑜‘𝑎) ∈ (Base‘𝑝)
24	22, 16	cfv 6561	. . . . . . . . . . 11 class (𝑜‘(𝑜‘𝑎))
25	24, 21	wceq 1540	. . . . . . . . . 10 wff (𝑜‘(𝑜‘𝑎)) = 𝑎
26		vb	. . . . . . . . . . . . 13 setvar 𝑏
27	26	cv 1539	. . . . . . . . . . . 12 class 𝑏
28		cple 17304	. . . . . . . . . . . . 13 class le
29	3, 28	cfv 6561	. . . . . . . . . . . 12 class (le‘𝑝)
30	21, 27, 29	wbr 5143	. . . . . . . . . . 11 wff 𝑎(le‘𝑝)𝑏
31	27, 16	cfv 6561	. . . . . . . . . . . 12 class (𝑜‘𝑏)
32	31, 22, 29	wbr 5143	. . . . . . . . . . 11 wff (𝑜‘𝑏)(le‘𝑝)(𝑜‘𝑎)
33	30, 32	wi 4	. . . . . . . . . 10 wff (𝑎(le‘𝑝)𝑏 → (𝑜‘𝑏)(le‘𝑝)(𝑜‘𝑎))
34	23, 25, 33	w3a 1087	. . . . . . . . 9 wff ((𝑜‘𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜‘𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜‘𝑏)(le‘𝑝)(𝑜‘𝑎)))
35		cjn 18357	. . . . . . . . . . . 12 class join
36	3, 35	cfv 6561	. . . . . . . . . . 11 class (join‘𝑝)
37	21, 22, 36	co 7431	. . . . . . . . . 10 class (𝑎(join‘𝑝)(𝑜‘𝑎))
38		cp1 18469	. . . . . . . . . . 11 class 1.
39	3, 38	cfv 6561	. . . . . . . . . 10 class (1.‘𝑝)
40	37, 39	wceq 1540	. . . . . . . . 9 wff (𝑎(join‘𝑝)(𝑜‘𝑎)) = (1.‘𝑝)
41		cmee 18358	. . . . . . . . . . . 12 class meet
42	3, 41	cfv 6561	. . . . . . . . . . 11 class (meet‘𝑝)
43	21, 22, 42	co 7431	. . . . . . . . . 10 class (𝑎(meet‘𝑝)(𝑜‘𝑎))
44		cp0 18468	. . . . . . . . . . 11 class 0.
45	3, 44	cfv 6561	. . . . . . . . . 10 class (0.‘𝑝)
46	43, 45	wceq 1540	. . . . . . . . 9 wff (𝑎(meet‘𝑝)(𝑜‘𝑎)) = (0.‘𝑝)
47	34, 40, 46	w3a 1087	. . . . . . . 8 wff (((𝑜‘𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜‘𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜‘𝑏)(le‘𝑝)(𝑜‘𝑎))) ∧ (𝑎(join‘𝑝)(𝑜‘𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜‘𝑎)) = (0.‘𝑝))
48	47, 26, 5	wral 3061	. . . . . . 7 wff ∀𝑏 ∈ (Base‘𝑝)(((𝑜‘𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜‘𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜‘𝑏)(le‘𝑝)(𝑜‘𝑎))) ∧ (𝑎(join‘𝑝)(𝑜‘𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜‘𝑎)) = (0.‘𝑝))
49	48, 20, 5	wral 3061	. . . . . 6 wff ∀𝑎 ∈ (Base‘𝑝)∀𝑏 ∈ (Base‘𝑝)(((𝑜‘𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜‘𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜‘𝑏)(le‘𝑝)(𝑜‘𝑎))) ∧ (𝑎(join‘𝑝)(𝑜‘𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜‘𝑎)) = (0.‘𝑝))
50	19, 49	wa 395	. . . . 5 wff (𝑜 = (oc‘𝑝) ∧ ∀𝑎 ∈ (Base‘𝑝)∀𝑏 ∈ (Base‘𝑝)(((𝑜‘𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜‘𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜‘𝑏)(le‘𝑝)(𝑜‘𝑎))) ∧ (𝑎(join‘𝑝)(𝑜‘𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜‘𝑎)) = (0.‘𝑝)))
51	50, 15	wex 1779	. . . 4 wff ∃𝑜(𝑜 = (oc‘𝑝) ∧ ∀𝑎 ∈ (Base‘𝑝)∀𝑏 ∈ (Base‘𝑝)(((𝑜‘𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜‘𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜‘𝑏)(le‘𝑝)(𝑜‘𝑎))) ∧ (𝑎(join‘𝑝)(𝑜‘𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜‘𝑎)) = (0.‘𝑝)))
52	14, 51	wa 395	. . 3 wff (((Base‘𝑝) ∈ dom (lub‘𝑝) ∧ (Base‘𝑝) ∈ dom (glb‘𝑝)) ∧ ∃𝑜(𝑜 = (oc‘𝑝) ∧ ∀𝑎 ∈ (Base‘𝑝)∀𝑏 ∈ (Base‘𝑝)(((𝑜‘𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜‘𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜‘𝑏)(le‘𝑝)(𝑜‘𝑎))) ∧ (𝑎(join‘𝑝)(𝑜‘𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜‘𝑎)) = (0.‘𝑝))))
53		cpo 18353	. . 3 class Poset
54	52, 2, 53	crab 3436	. 2 class {𝑝 ∈ Poset ∣ (((Base‘𝑝) ∈ dom (lub‘𝑝) ∧ (Base‘𝑝) ∈ dom (glb‘𝑝)) ∧ ∃𝑜(𝑜 = (oc‘𝑝) ∧ ∀𝑎 ∈ (Base‘𝑝)∀𝑏 ∈ (Base‘𝑝)(((𝑜‘𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜‘𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜‘𝑏)(le‘𝑝)(𝑜‘𝑎))) ∧ (𝑎(join‘𝑝)(𝑜‘𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜‘𝑎)) = (0.‘𝑝))))}
55	1, 54	wceq 1540	1 wff OP = {𝑝 ∈ Poset ∣ (((Base‘𝑝) ∈ dom (lub‘𝑝) ∧ (Base‘𝑝) ∈ dom (glb‘𝑝)) ∧ ∃𝑜(𝑜 = (oc‘𝑝) ∧ ∀𝑎 ∈ (Base‘𝑝)∀𝑏 ∈ (Base‘𝑝)(((𝑜‘𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜‘𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜‘𝑏)(le‘𝑝)(𝑜‘𝑎))) ∧ (𝑎(join‘𝑝)(𝑜‘𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜‘𝑎)) = (0.‘𝑝))))}

This definition is referenced by:  isopos  39181