Metamath Proof Explorer

Definition 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 ∈ Poset | Base p ∈ dom ⁡ lub ⁡ p ∧ Base p ∈ dom ⁡ glb ⁡ p ∧ ∃ o o = oc ⁡ p ∧ ∀ a ∈ Base p ∀ b ∈ Base p o ⁡ a ∈ Base p ∧ o ⁡ o ⁡ a = a ∧ a ≤ p b → o ⁡ b ≤ p o ⁡ a ∧ a join ⁡ p o ⁡ a = 1. ⁡ p ∧ 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 ∈ 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 ∈ dom ⁡ glb ⁡ p
14 9 13 wa wff Base p ∈ dom ⁡ lub ⁡ p ∧ Base p ∈ 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 ∈ 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 ≤ p
29 21 cv setvar b
30 22 29 28 wbr wff a ≤ p b
31 29 16 cfv class o ⁡ b
32 31 23 28 wbr wff o ⁡ b ≤ p o ⁡ a
33 30 32 wi wff a ≤ p b → o ⁡ b ≤ p o ⁡ a
34 24 26 33 w3a wff o ⁡ a ∈ Base p ∧ o ⁡ o ⁡ a = a ∧ a ≤ p b → o ⁡ b ≤ 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 ∈ Base p ∧ o ⁡ o ⁡ a = a ∧ a ≤ p b → o ⁡ b ≤ p o ⁡ a ∧ a join ⁡ p o ⁡ a = 1. ⁡ p ∧ a meet ⁡ p o ⁡ a = 0. ⁡ p
48 47 21 5 wral wff ∀ b ∈ Base p o ⁡ a ∈ Base p ∧ o ⁡ o ⁡ a = a ∧ a ≤ p b → o ⁡ b ≤ p o ⁡ a ∧ a join ⁡ p o ⁡ a = 1. ⁡ p ∧ a meet ⁡ p o ⁡ a = 0. ⁡ p
49 48 20 5 wral wff ∀ a ∈ Base p ∀ b ∈ Base p o ⁡ a ∈ Base p ∧ o ⁡ o ⁡ a = a ∧ a ≤ p b → o ⁡ b ≤ p o ⁡ a ∧ a join ⁡ p o ⁡ a = 1. ⁡ p ∧ a meet ⁡ p o ⁡ a = 0. ⁡ p
50 19 49 wa wff o = oc ⁡ p ∧ ∀ a ∈ Base p ∀ b ∈ Base p o ⁡ a ∈ Base p ∧ o ⁡ o ⁡ a = a ∧ a ≤ p b → o ⁡ b ≤ p o ⁡ a ∧ a join ⁡ p o ⁡ a = 1. ⁡ p ∧ a meet ⁡ p o ⁡ a = 0. ⁡ p
51 50 15 wex wff ∃ o o = oc ⁡ p ∧ ∀ a ∈ Base p ∀ b ∈ Base p o ⁡ a ∈ Base p ∧ o ⁡ o ⁡ a = a ∧ a ≤ p b → o ⁡ b ≤ p o ⁡ a ∧ a join ⁡ p o ⁡ a = 1. ⁡ p ∧ a meet ⁡ p o ⁡ a = 0. ⁡ p
52 14 51 wa wff Base p ∈ dom ⁡ lub ⁡ p ∧ Base p ∈ dom ⁡ glb ⁡ p ∧ ∃ o o = oc ⁡ p ∧ ∀ a ∈ Base p ∀ b ∈ Base p o ⁡ a ∈ Base p ∧ o ⁡ o ⁡ a = a ∧ a ≤ p b → o ⁡ b ≤ p o ⁡ a ∧ a join ⁡ p o ⁡ a = 1. ⁡ p ∧ a meet ⁡ p o ⁡ a = 0. ⁡ p
53 52 1 2 crab class p ∈ Poset | Base p ∈ dom ⁡ lub ⁡ p ∧ Base p ∈ dom ⁡ glb ⁡ p ∧ ∃ o o = oc ⁡ p ∧ ∀ a ∈ Base p ∀ b ∈ Base p o ⁡ a ∈ Base p ∧ o ⁡ o ⁡ a = a ∧ a ≤ p b → o ⁡ b ≤ p o ⁡ a ∧ a join ⁡ p o ⁡ a = 1. ⁡ p ∧ a meet ⁡ p o ⁡ a = 0. ⁡ p
54 0 53 wceq wff OP = p ∈ Poset | Base p ∈ dom ⁡ lub ⁡ p ∧ Base p ∈ dom ⁡ glb ⁡ p ∧ ∃ o o = oc ⁡ p ∧ ∀ a ∈ Base p ∀ b ∈ Base p o ⁡ a ∈ Base p ∧ o ⁡ o ⁡ a = a ∧ a ≤ p b → o ⁡ b ≤ p o ⁡ a ∧ a join ⁡ p o ⁡ a = 1. ⁡ p ∧ a meet ⁡ p o ⁡ a = 0. ⁡ p