df-oposet - Mathbox for Norm Megill

	Mathbox for Norm Megill	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-oposet		Unicode version

Definition df-oposet 29659

Description: Define the class of orthoposets. (Contributed by NM, 20-Oct-2011.)

**Assertion**
Ref	Expression
df-oposet	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Distinct variable group:

**Detailed syntax breakdown of Definition df-oposet**
Step	Hyp	Ref	Expression
1		cops 29655	. 2
2		vp	. . . . . . . 8
3	2	cv 1648	. . . . . . 7
4		cp0 14421	. . . . . . 7
5	3, 4	cfv 5413	. . . . . 6
6		cbs 13424	. . . . . . 7
7	3, 6	cfv 5413	. . . . . 6
8	5, 7	wcel 1721	. . . . 5
9		cp1 14422	. . . . . . 7
10	3, 9	cfv 5413	. . . . . 6
11	10, 7	wcel 1721	. . . . 5
12	8, 11	wa 359	. . . 4 $/\$
13		vo	. . . . . . . 8
14	13	cv 1648	. . . . . . 7
15		coc 13492	. . . . . . . 8
16	3, 15	cfv 5413	. . . . . . 7
17	14, 16	wceq 1649	. . . . . 6
18		va	. . . . . . . . . . . . 13
19	18	cv 1648	. . . . . . . . . . . 12
20	19, 14	cfv 5413	. . . . . . . . . . 11
21	20, 7	wcel 1721	. . . . . . . . . 10
22	20, 14	cfv 5413	. . . . . . . . . . 11
23	22, 19	wceq 1649	. . . . . . . . . 10
24		vb	. . . . . . . . . . . . 13
25	24	cv 1648	. . . . . . . . . . . 12
26		cple 13491	. . . . . . . . . . . . 13
27	3, 26	cfv 5413	. . . . . . . . . . . 12
28	19, 25, 27	wbr 4172	. . . . . . . . . . 11
29	25, 14	cfv 5413	. . . . . . . . . . . 12
30	29, 20, 27	wbr 4172	. . . . . . . . . . 11
31	28, 30	wi 4	. . . . . . . . . 10
32	21, 23, 31	w3a 936	. . . . . . . . 9 $/\$ $/\$
33		cjn 14356	. . . . . . . . . . . 12
34	3, 33	cfv 5413	. . . . . . . . . . 11
35	19, 20, 34	co 6040	. . . . . . . . . 10
36	35, 10	wceq 1649	. . . . . . . . 9
37		cmee 14357	. . . . . . . . . . . 12
38	3, 37	cfv 5413	. . . . . . . . . . 11
39	19, 20, 38	co 6040	. . . . . . . . . 10
40	39, 5	wceq 1649	. . . . . . . . 9
41	32, 36, 40	w3a 936	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
42	41, 24, 7	wral 2666	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
43	42, 18, 7	wral 2666	. . . . . 6 $/\$ $/\$ $/\$ $/\$
44	17, 43	wa 359	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
45	44, 13	wex 1547	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
46	12, 45	wa 359	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47		cpo 14352	. . 3
48	46, 2, 47	crab 2670	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49	1, 48	wceq 1649	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Colors of variables: wff set class

This definition is referenced by: isopos 29663

W3C validator