df-oposet

Description: Define the class of orthoposets, which are bounded posets with an orthocomplementation operation. Note that ( Base p ) e. dom ( lub p ) 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)

		Ref	Expression
	Assertion	df-oposet	$⊢ OP = \{p \in Poset \| (({Base}_{p} \in dom lub (p) \land {Base}_{p} \in dom glb (p)) \land \exists o (o = oc (p) \land \forall a \in {Base}_{p} \forall b \in {Base}_{p} ((o (a) \in {Base}_{p} \land o (o (a)) = a \land (a \leq_{p} b \to o (b) \leq_{p} o (a))) \land a join (p) o (a) = 1. (p) \land a meet (p) o (a) = 0. (p))))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cops	$class OP$
1		vp	$setvar p$
2		cpo	$class Poset$
3		cbs	$class Base$
4	1	cv	$setvar p$
5	4 3	cfv	$class {Base}_{p}$
6		club	$class lub$
7	4 6	cfv	$class lub (p)$
8	7	cdm	$class dom lub (p)$
9	5 8	wcel	$wff {Base}_{p} \in dom lub (p)$
10		cglb	$class glb$
11	4 10	cfv	$class glb (p)$
12	11	cdm	$class dom glb (p)$
13	5 12	wcel	$wff {Base}_{p} \in dom glb (p)$
14	9 13	wa	$wff ({Base}_{p} \in dom lub (p) \land {Base}_{p} \in dom glb (p))$
15		vo	$setvar o$
16	15	cv	$setvar o$
17		coc	$class oc$
18	4 17	cfv	$class oc (p)$
19	16 18	wceq	$wff o = oc (p)$
20		va	$setvar a$
21		vb	$setvar b$
22	20	cv	$setvar a$
23	22 16	cfv	$class o (a)$
24	23 5	wcel	$wff o (a) \in {Base}_{p}$
25	23 16	cfv	$class o (o (a))$
26	25 22	wceq	$wff o (o (a)) = a$
27		cple	$class le$
28	4 27	cfv	$class \leq_{p}$
29	21	cv	$setvar b$
30	22 29 28	wbr	$wff a \leq_{p} b$
31	29 16	cfv	$class o (b)$
32	31 23 28	wbr	$wff o (b) \leq_{p} o (a)$
33	30 32	wi	$wff (a \leq_{p} b \to o (b) \leq_{p} o (a))$
34	24 26 33	w3a	$wff (o (a) \in {Base}_{p} \land o (o (a)) = a \land (a \leq_{p} b \to o (b) \leq_{p} o (a)))$
35		cjn	$class join$
36	4 35	cfv	$class join (p)$
37	22 23 36	co	$class (a join (p) o (a))$
38		cp1	$class 1.$
39	4 38	cfv	$class 1. (p)$
40	37 39	wceq	$wff a join (p) o (a) = 1. (p)$
41		cmee	$class meet$
42	4 41	cfv	$class meet (p)$
43	22 23 42	co	$class (a meet (p) o (a))$
44		cp0	$class 0.$
45	4 44	cfv	$class 0. (p)$
46	43 45	wceq	$wff a meet (p) o (a) = 0. (p)$
47	34 40 46	w3a	$wff ((o (a) \in {Base}_{p} \land o (o (a)) = a \land (a \leq_{p} b \to o (b) \leq_{p} o (a))) \land a join (p) o (a) = 1. (p) \land a meet (p) o (a) = 0. (p))$
48	47 21 5	wral	$wff \forall b \in {Base}_{p} ((o (a) \in {Base}_{p} \land o (o (a)) = a \land (a \leq_{p} b \to o (b) \leq_{p} o (a))) \land a join (p) o (a) = 1. (p) \land a meet (p) o (a) = 0. (p))$
49	48 20 5	wral	$wff \forall a \in {Base}_{p} \forall b \in {Base}_{p} ((o (a) \in {Base}_{p} \land o (o (a)) = a \land (a \leq_{p} b \to o (b) \leq_{p} o (a))) \land a join (p) o (a) = 1. (p) \land a meet (p) o (a) = 0. (p))$
50	19 49	wa	$wff (o = oc (p) \land \forall a \in {Base}_{p} \forall b \in {Base}_{p} ((o (a) \in {Base}_{p} \land o (o (a)) = a \land (a \leq_{p} b \to o (b) \leq_{p} o (a))) \land a join (p) o (a) = 1. (p) \land a meet (p) o (a) = 0. (p)))$
51	50 15	wex	$wff \exists o (o = oc (p) \land \forall a \in {Base}_{p} \forall b \in {Base}_{p} ((o (a) \in {Base}_{p} \land o (o (a)) = a \land (a \leq_{p} b \to o (b) \leq_{p} o (a))) \land a join (p) o (a) = 1. (p) \land a meet (p) o (a) = 0. (p)))$
52	14 51	wa	$wff (({Base}_{p} \in dom lub (p) \land {Base}_{p} \in dom glb (p)) \land \exists o (o = oc (p) \land \forall a \in {Base}_{p} \forall b \in {Base}_{p} ((o (a) \in {Base}_{p} \land o (o (a)) = a \land (a \leq_{p} b \to o (b) \leq_{p} o (a))) \land a join (p) o (a) = 1. (p) \land a meet (p) o (a) = 0. (p))))$
53	52 1 2	crab	$class \{p \in Poset \| (({Base}_{p} \in dom lub (p) \land {Base}_{p} \in dom glb (p)) \land \exists o (o = oc (p) \land \forall a \in {Base}_{p} \forall b \in {Base}_{p} ((o (a) \in {Base}_{p} \land o (o (a)) = a \land (a \leq_{p} b \to o (b) \leq_{p} o (a))) \land a join (p) o (a) = 1. (p) \land a meet (p) o (a) = 0. (p))))\}$
54	0 53	wceq	$wff OP = \{p \in Poset \| (({Base}_{p} \in dom lub (p) \land {Base}_{p} \in dom glb (p)) \land \exists o (o = oc (p) \land \forall a \in {Base}_{p} \forall b \in {Base}_{p} ((o (a) \in {Base}_{p} \land o (o (a)) = a \land (a \leq_{p} b \to o (b) \leq_{p} o (a))) \land a join (p) o (a) = 1. (p) \land a meet (p) o (a) = 0. (p))))\}$

Metamath Proof Explorer

Definition df-oposet

Detailed syntax breakdown