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 = { 𝑝 ∈ Poset ∣ ( ( ( Base ‘ 𝑝 ) ∈ dom ( lub ‘ 𝑝 ) ∧ ( Base ‘ 𝑝 ) ∈ dom ( glb ‘ 𝑝 ) ) ∧ ∃ 𝑜 ( 𝑜 = ( oc ‘ 𝑝 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑝 ) ∀ 𝑏 ∈ ( Base ‘ 𝑝 ) ( ( ( 𝑜 ‘ 𝑎 ) ∈ ( Base ‘ 𝑝 ) ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑎 ) ) = 𝑎 ∧ ( 𝑎 ( le ‘ 𝑝 ) 𝑏 → ( 𝑜 ‘ 𝑏 ) ( le ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) ) ∧ ( 𝑎 ( join ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) = ( 1. ‘ 𝑝 ) ∧ ( 𝑎 ( meet ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) = ( 0. ‘ 𝑝 ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cops ⊢ OP
1 vp ⊢ 𝑝
2 cpo ⊢ Poset
3 cbs ⊢ Base
4 1 cv ⊢ 𝑝
5 4 3 cfv ⊢ ( Base ‘ 𝑝 )
6 club ⊢ lub
7 4 6 cfv ⊢ ( lub ‘ 𝑝 )
8 7 cdm ⊢ dom ( lub ‘ 𝑝 )
9 5 8 wcel ⊢ ( Base ‘ 𝑝 ) ∈ dom ( lub ‘ 𝑝 )
10 cglb ⊢ glb
11 4 10 cfv ⊢ ( glb ‘ 𝑝 )
12 11 cdm ⊢ dom ( glb ‘ 𝑝 )
13 5 12 wcel ⊢ ( Base ‘ 𝑝 ) ∈ dom ( glb ‘ 𝑝 )
14 9 13 wa ⊢ ( ( Base ‘ 𝑝 ) ∈ dom ( lub ‘ 𝑝 ) ∧ ( Base ‘ 𝑝 ) ∈ dom ( glb ‘ 𝑝 ) )
15 vo ⊢ 𝑜
16 15 cv ⊢ 𝑜
17 coc ⊢ oc
18 4 17 cfv ⊢ ( oc ‘ 𝑝 )
19 16 18 wceq ⊢ 𝑜 = ( oc ‘ 𝑝 )
20 va ⊢ 𝑎
21 vb ⊢ 𝑏
22 20 cv ⊢ 𝑎
23 22 16 cfv ⊢ ( 𝑜 ‘ 𝑎 )
24 23 5 wcel ⊢ ( 𝑜 ‘ 𝑎 ) ∈ ( Base ‘ 𝑝 )
25 23 16 cfv ⊢ ( 𝑜 ‘ ( 𝑜 ‘ 𝑎 ) )
26 25 22 wceq ⊢ ( 𝑜 ‘ ( 𝑜 ‘ 𝑎 ) ) = 𝑎
27 cple ⊢ le
28 4 27 cfv ⊢ ( le ‘ 𝑝 )
29 21 cv ⊢ 𝑏
30 22 29 28 wbr ⊢ 𝑎 ( le ‘ 𝑝 ) 𝑏
31 29 16 cfv ⊢ ( 𝑜 ‘ 𝑏 )
32 31 23 28 wbr ⊢ ( 𝑜 ‘ 𝑏 ) ( le ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 )
33 30 32 wi ⊢ ( 𝑎 ( le ‘ 𝑝 ) 𝑏 → ( 𝑜 ‘ 𝑏 ) ( le ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) )
34 24 26 33 w3a ⊢ ( ( 𝑜 ‘ 𝑎 ) ∈ ( Base ‘ 𝑝 ) ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑎 ) ) = 𝑎 ∧ ( 𝑎 ( le ‘ 𝑝 ) 𝑏 → ( 𝑜 ‘ 𝑏 ) ( le ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) )
35 cjn ⊢ join
36 4 35 cfv ⊢ ( join ‘ 𝑝 )
37 22 23 36 co ⊢ ( 𝑎 ( join ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) )
38 cp1 ⊢ 1.
39 4 38 cfv ⊢ ( 1. ‘ 𝑝 )
40 37 39 wceq ⊢ ( 𝑎 ( join ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) = ( 1. ‘ 𝑝 )
41 cmee ⊢ meet
42 4 41 cfv ⊢ ( meet ‘ 𝑝 )
43 22 23 42 co ⊢ ( 𝑎 ( meet ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) )
44 cp0 ⊢ 0.
45 4 44 cfv ⊢ ( 0. ‘ 𝑝 )
46 43 45 wceq ⊢ ( 𝑎 ( meet ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) = ( 0. ‘ 𝑝 )
47 34 40 46 w3a ⊢ ( ( ( 𝑜 ‘ 𝑎 ) ∈ ( Base ‘ 𝑝 ) ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑎 ) ) = 𝑎 ∧ ( 𝑎 ( le ‘ 𝑝 ) 𝑏 → ( 𝑜 ‘ 𝑏 ) ( le ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) ) ∧ ( 𝑎 ( join ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) = ( 1. ‘ 𝑝 ) ∧ ( 𝑎 ( meet ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) = ( 0. ‘ 𝑝 ) )
48 47 21 5 wral ⊢ ∀ 𝑏 ∈ ( Base ‘ 𝑝 ) ( ( ( 𝑜 ‘ 𝑎 ) ∈ ( Base ‘ 𝑝 ) ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑎 ) ) = 𝑎 ∧ ( 𝑎 ( le ‘ 𝑝 ) 𝑏 → ( 𝑜 ‘ 𝑏 ) ( le ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) ) ∧ ( 𝑎 ( join ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) = ( 1. ‘ 𝑝 ) ∧ ( 𝑎 ( meet ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) = ( 0. ‘ 𝑝 ) )
49 48 20 5 wral ⊢ ∀ 𝑎 ∈ ( Base ‘ 𝑝 ) ∀ 𝑏 ∈ ( Base ‘ 𝑝 ) ( ( ( 𝑜 ‘ 𝑎 ) ∈ ( Base ‘ 𝑝 ) ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑎 ) ) = 𝑎 ∧ ( 𝑎 ( le ‘ 𝑝 ) 𝑏 → ( 𝑜 ‘ 𝑏 ) ( le ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) ) ∧ ( 𝑎 ( join ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) = ( 1. ‘ 𝑝 ) ∧ ( 𝑎 ( meet ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) = ( 0. ‘ 𝑝 ) )
50 19 49 wa ⊢ ( 𝑜 = ( oc ‘ 𝑝 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑝 ) ∀ 𝑏 ∈ ( Base ‘ 𝑝 ) ( ( ( 𝑜 ‘ 𝑎 ) ∈ ( Base ‘ 𝑝 ) ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑎 ) ) = 𝑎 ∧ ( 𝑎 ( le ‘ 𝑝 ) 𝑏 → ( 𝑜 ‘ 𝑏 ) ( le ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) ) ∧ ( 𝑎 ( join ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) = ( 1. ‘ 𝑝 ) ∧ ( 𝑎 ( meet ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) = ( 0. ‘ 𝑝 ) ) )
51 50 15 wex ⊢ ∃ 𝑜 ( 𝑜 = ( oc ‘ 𝑝 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑝 ) ∀ 𝑏 ∈ ( Base ‘ 𝑝 ) ( ( ( 𝑜 ‘ 𝑎 ) ∈ ( Base ‘ 𝑝 ) ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑎 ) ) = 𝑎 ∧ ( 𝑎 ( le ‘ 𝑝 ) 𝑏 → ( 𝑜 ‘ 𝑏 ) ( le ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) ) ∧ ( 𝑎 ( join ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) = ( 1. ‘ 𝑝 ) ∧ ( 𝑎 ( meet ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) = ( 0. ‘ 𝑝 ) ) )
52 14 51 wa ⊢ ( ( ( Base ‘ 𝑝 ) ∈ dom ( lub ‘ 𝑝 ) ∧ ( Base ‘ 𝑝 ) ∈ dom ( glb ‘ 𝑝 ) ) ∧ ∃ 𝑜 ( 𝑜 = ( oc ‘ 𝑝 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑝 ) ∀ 𝑏 ∈ ( Base ‘ 𝑝 ) ( ( ( 𝑜 ‘ 𝑎 ) ∈ ( Base ‘ 𝑝 ) ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑎 ) ) = 𝑎 ∧ ( 𝑎 ( le ‘ 𝑝 ) 𝑏 → ( 𝑜 ‘ 𝑏 ) ( le ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) ) ∧ ( 𝑎 ( join ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) = ( 1. ‘ 𝑝 ) ∧ ( 𝑎 ( meet ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) = ( 0. ‘ 𝑝 ) ) ) )
53 52 1 2 crab ⊢ { 𝑝 ∈ Poset ∣ ( ( ( Base ‘ 𝑝 ) ∈ dom ( lub ‘ 𝑝 ) ∧ ( Base ‘ 𝑝 ) ∈ dom ( glb ‘ 𝑝 ) ) ∧ ∃ 𝑜 ( 𝑜 = ( oc ‘ 𝑝 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑝 ) ∀ 𝑏 ∈ ( Base ‘ 𝑝 ) ( ( ( 𝑜 ‘ 𝑎 ) ∈ ( Base ‘ 𝑝 ) ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑎 ) ) = 𝑎 ∧ ( 𝑎 ( le ‘ 𝑝 ) 𝑏 → ( 𝑜 ‘ 𝑏 ) ( le ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) ) ∧ ( 𝑎 ( join ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) = ( 1. ‘ 𝑝 ) ∧ ( 𝑎 ( meet ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) = ( 0. ‘ 𝑝 ) ) ) ) }
54 0 53 wceq ⊢ OP = { 𝑝 ∈ Poset ∣ ( ( ( Base ‘ 𝑝 ) ∈ dom ( lub ‘ 𝑝 ) ∧ ( Base ‘ 𝑝 ) ∈ dom ( glb ‘ 𝑝 ) ) ∧ ∃ 𝑜 ( 𝑜 = ( oc ‘ 𝑝 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑝 ) ∀ 𝑏 ∈ ( Base ‘ 𝑝 ) ( ( ( 𝑜 ‘ 𝑎 ) ∈ ( Base ‘ 𝑝 ) ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑎 ) ) = 𝑎 ∧ ( 𝑎 ( le ‘ 𝑝 ) 𝑏 → ( 𝑜 ‘ 𝑏 ) ( le ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) ) ∧ ( 𝑎 ( join ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) = ( 1. ‘ 𝑝 ) ∧ ( 𝑎 ( meet ‘ 𝑝 ) ( 𝑜 ‘ 𝑎 ) ) = ( 0. ‘ 𝑝 ) ) ) ) }