df-oposet - Mathbox for Norm Megill

	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 34463

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**
Step	Hyp	Ref	Expression
1		cops 34459	. 2
2		vp	. . . . . . . 8
3	2	cv 1482	. . . . . . 7
4		cbs 15857	. . . . . . 7
5	3, 4	cfv 5888	. . . . . 6
6		club 16942	. . . . . . . 8
7	3, 6	cfv 5888	. . . . . . 7
8	7	cdm 5114	. . . . . 6
9	5, 8	wcel 1990	. . . . 5
10		cglb 16943	. . . . . . . 8
11	3, 10	cfv 5888	. . . . . . 7
12	11	cdm 5114	. . . . . 6
13	5, 12	wcel 1990	. . . . 5
14	9, 13	wa 384	. . . 4 $/\$
15		vo	. . . . . . . 8
16	15	cv 1482	. . . . . . 7
17		coc 15949	. . . . . . . 8
18	3, 17	cfv 5888	. . . . . . 7
19	16, 18	wceq 1483	. . . . . 6
20		va	. . . . . . . . . . . . 13
21	20	cv 1482	. . . . . . . . . . . 12
22	21, 16	cfv 5888	. . . . . . . . . . 11
23	22, 5	wcel 1990	. . . . . . . . . 10
24	22, 16	cfv 5888	. . . . . . . . . . 11
25	24, 21	wceq 1483	. . . . . . . . . 10
26		vb	. . . . . . . . . . . . 13
27	26	cv 1482	. . . . . . . . . . . 12
28		cple 15948	. . . . . . . . . . . . 13
29	3, 28	cfv 5888	. . . . . . . . . . . 12
30	21, 27, 29	wbr 4653	. . . . . . . . . . 11
31	27, 16	cfv 5888	. . . . . . . . . . . 12
32	31, 22, 29	wbr 4653	. . . . . . . . . . 11
33	30, 32	wi 4	. . . . . . . . . 10
34	23, 25, 33	w3a 1037	. . . . . . . . 9 $/\$ $/\$
35		cjn 16944	. . . . . . . . . . . 12
36	3, 35	cfv 5888	. . . . . . . . . . 11
37	21, 22, 36	co 6650	. . . . . . . . . 10
38		cp1 17038	. . . . . . . . . . 11
39	3, 38	cfv 5888	. . . . . . . . . 10
40	37, 39	wceq 1483	. . . . . . . . 9
41		cmee 16945	. . . . . . . . . . . 12
42	3, 41	cfv 5888	. . . . . . . . . . 11
43	21, 22, 42	co 6650	. . . . . . . . . 10
44		cp0 17037	. . . . . . . . . . 11
45	3, 44	cfv 5888	. . . . . . . . . 10
46	43, 45	wceq 1483	. . . . . . . . 9
47	34, 40, 46	w3a 1037	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
48	47, 26, 5	wral 2912	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
49	48, 20, 5	wral 2912	. . . . . 6 $/\$ $/\$ $/\$ $/\$
50	19, 49	wa 384	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
51	50, 15	wex 1704	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
52	14, 51	wa 384	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53		cpo 16940	. . 3
54	52, 2, 53	crab 2916	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	1, 54	wceq 1483	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

This definition is referenced by: isopos 34467

W3C validator