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 Unicode version

Definition df-oposet 35002

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 34998	. 2
2		vp	. . . . . . . 8
3	2	cv 1394	. . . . . . 7
4		cbs 14643	. . . . . . 7
5	3, 4	cfv 5594	. . . . . 6
6		club 15697	. . . . . . . 8
7	3, 6	cfv 5594	. . . . . . 7
8	7	cdm 5008	. . . . . 6
9	5, 8	wcel 1819	. . . . 5
10		cglb 15698	. . . . . . . 8
11	3, 10	cfv 5594	. . . . . . 7
12	11	cdm 5008	. . . . . 6
13	5, 12	wcel 1819	. . . . 5
14	9, 13	wa 369	. . . 4 $/\$
15		vo	. . . . . . . 8
16	15	cv 1394	. . . . . . 7
17		coc 14719	. . . . . . . 8
18	3, 17	cfv 5594	. . . . . . 7
19	16, 18	wceq 1395	. . . . . 6
20		va	. . . . . . . . . . . . 13
21	20	cv 1394	. . . . . . . . . . . 12
22	21, 16	cfv 5594	. . . . . . . . . . 11
23	22, 5	wcel 1819	. . . . . . . . . 10
24	22, 16	cfv 5594	. . . . . . . . . . 11
25	24, 21	wceq 1395	. . . . . . . . . 10
26		vb	. . . . . . . . . . . . 13
27	26	cv 1394	. . . . . . . . . . . 12
28		cple 14718	. . . . . . . . . . . . 13
29	3, 28	cfv 5594	. . . . . . . . . . . 12
30	21, 27, 29	wbr 4456	. . . . . . . . . . 11
31	27, 16	cfv 5594	. . . . . . . . . . . 12
32	31, 22, 29	wbr 4456	. . . . . . . . . . 11
33	30, 32	wi 4	. . . . . . . . . 10
34	23, 25, 33	w3a 973	. . . . . . . . 9 $/\$ $/\$
35		cjn 15699	. . . . . . . . . . . 12
36	3, 35	cfv 5594	. . . . . . . . . . 11
37	21, 22, 36	co 6296	. . . . . . . . . 10
38		cp1 15794	. . . . . . . . . . 11
39	3, 38	cfv 5594	. . . . . . . . . 10
40	37, 39	wceq 1395	. . . . . . . . 9
41		cmee 15700	. . . . . . . . . . . 12
42	3, 41	cfv 5594	. . . . . . . . . . 11
43	21, 22, 42	co 6296	. . . . . . . . . 10
44		cp0 15793	. . . . . . . . . . 11
45	3, 44	cfv 5594	. . . . . . . . . 10
46	43, 45	wceq 1395	. . . . . . . . 9
47	34, 40, 46	w3a 973	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
48	47, 26, 5	wral 2807	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
49	48, 20, 5	wral 2807	. . . . . 6 $/\$ $/\$ $/\$ $/\$
50	19, 49	wa 369	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
51	50, 15	wex 1613	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
52	14, 51	wa 369	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53		cpo 15695	. . 3
54	52, 2, 53	crab 2811	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	1, 54	wceq 1395	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

This definition is referenced by: isopos 35006

W3C validator