![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > op01dm | Structured version Visualization version GIF version |
Description: Conditions necessary for zero and unit elements to exist. (Contributed by NM, 14-Sep-2018.) |
Ref | Expression |
---|---|
op01dm.b | ⊢ 𝐵 = (Base‘𝐾) |
op01dm.u | ⊢ 𝑈 = (lub‘𝐾) |
op01dm.g | ⊢ 𝐺 = (glb‘𝐾) |
Ref | Expression |
---|---|
op01dm | ⊢ (𝐾 ∈ OP → (𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | op01dm.b | . . 3 ⊢ 𝐵 = (Base‘𝐾) | |
2 | op01dm.u | . . 3 ⊢ 𝑈 = (lub‘𝐾) | |
3 | op01dm.g | . . 3 ⊢ 𝐺 = (glb‘𝐾) | |
4 | eqid 2824 | . . 3 ⊢ (le‘𝐾) = (le‘𝐾) | |
5 | eqid 2824 | . . 3 ⊢ (oc‘𝐾) = (oc‘𝐾) | |
6 | eqid 2824 | . . 3 ⊢ (join‘𝐾) = (join‘𝐾) | |
7 | eqid 2824 | . . 3 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
8 | eqid 2824 | . . 3 ⊢ (0.‘𝐾) = (0.‘𝐾) | |
9 | eqid 2824 | . . 3 ⊢ (1.‘𝐾) = (1.‘𝐾) | |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | isopos 35254 | . 2 ⊢ (𝐾 ∈ OP ↔ ((𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((((oc‘𝐾)‘𝑥) ∈ 𝐵 ∧ ((oc‘𝐾)‘((oc‘𝐾)‘𝑥)) = 𝑥 ∧ (𝑥(le‘𝐾)𝑦 → ((oc‘𝐾)‘𝑦)(le‘𝐾)((oc‘𝐾)‘𝑥))) ∧ (𝑥(join‘𝐾)((oc‘𝐾)‘𝑥)) = (1.‘𝐾) ∧ (𝑥(meet‘𝐾)((oc‘𝐾)‘𝑥)) = (0.‘𝐾)))) |
11 | simpl 476 | . . 3 ⊢ (((𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((((oc‘𝐾)‘𝑥) ∈ 𝐵 ∧ ((oc‘𝐾)‘((oc‘𝐾)‘𝑥)) = 𝑥 ∧ (𝑥(le‘𝐾)𝑦 → ((oc‘𝐾)‘𝑦)(le‘𝐾)((oc‘𝐾)‘𝑥))) ∧ (𝑥(join‘𝐾)((oc‘𝐾)‘𝑥)) = (1.‘𝐾) ∧ (𝑥(meet‘𝐾)((oc‘𝐾)‘𝑥)) = (0.‘𝐾))) → (𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺)) | |
12 | 11 | 3adantl1 1213 | . 2 ⊢ (((𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((((oc‘𝐾)‘𝑥) ∈ 𝐵 ∧ ((oc‘𝐾)‘((oc‘𝐾)‘𝑥)) = 𝑥 ∧ (𝑥(le‘𝐾)𝑦 → ((oc‘𝐾)‘𝑦)(le‘𝐾)((oc‘𝐾)‘𝑥))) ∧ (𝑥(join‘𝐾)((oc‘𝐾)‘𝑥)) = (1.‘𝐾) ∧ (𝑥(meet‘𝐾)((oc‘𝐾)‘𝑥)) = (0.‘𝐾))) → (𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺)) |
13 | 10, 12 | sylbi 209 | 1 ⊢ (𝐾 ∈ OP → (𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1113 = wceq 1658 ∈ wcel 2166 ∀wral 3116 class class class wbr 4872 dom cdm 5341 ‘cfv 6122 (class class class)co 6904 Basecbs 16221 lecple 16311 occoc 16312 Posetcpo 17292 lubclub 17294 glbcglb 17295 joincjn 17296 meetcmee 17297 0.cp0 17389 1.cp1 17390 OPcops 35246 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2390 ax-ext 2802 ax-nul 5012 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2604 df-eu 2639 df-clab 2811 df-cleq 2817 df-clel 2820 df-nfc 2957 df-ral 3121 df-rex 3122 df-rab 3125 df-v 3415 df-sbc 3662 df-dif 3800 df-un 3802 df-in 3804 df-ss 3811 df-nul 4144 df-if 4306 df-sn 4397 df-pr 4399 df-op 4403 df-uni 4658 df-br 4873 df-dm 5351 df-iota 6085 df-fv 6130 df-ov 6907 df-oposet 35250 |
This theorem is referenced by: op0cl 35258 op1cl 35259 op0le 35260 ople1 35265 lhp2lt 36075 |
Copyright terms: Public domain | W3C validator |