# Metamath Proof Explorer

## Theorem op01dm

Description: Conditions necessary for zero and unit elements to exist. (Contributed by NM, 14-Sep-2018)

Ref Expression
Hypotheses op01dm.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
op01dm.u ${⊢}{U}=\mathrm{lub}\left({K}\right)$
op01dm.g ${⊢}{G}=\mathrm{glb}\left({K}\right)$
Assertion op01dm ${⊢}{K}\in \mathrm{OP}\to \left({B}\in \mathrm{dom}{U}\wedge {B}\in \mathrm{dom}{G}\right)$

### Proof

Step Hyp Ref Expression
1 op01dm.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 op01dm.u ${⊢}{U}=\mathrm{lub}\left({K}\right)$
3 op01dm.g ${⊢}{G}=\mathrm{glb}\left({K}\right)$
4 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
5 eqid ${⊢}\mathrm{oc}\left({K}\right)=\mathrm{oc}\left({K}\right)$
6 eqid ${⊢}\mathrm{join}\left({K}\right)=\mathrm{join}\left({K}\right)$
7 eqid ${⊢}\mathrm{meet}\left({K}\right)=\mathrm{meet}\left({K}\right)$
8 eqid ${⊢}\mathrm{0.}\left({K}\right)=\mathrm{0.}\left({K}\right)$
9 eqid ${⊢}\mathrm{1.}\left({K}\right)=\mathrm{1.}\left({K}\right)$
10 1 2 3 4 5 6 7 8 9 isopos ${⊢}{K}\in \mathrm{OP}↔\left(\left({K}\in \mathrm{Poset}\wedge {B}\in \mathrm{dom}{U}\wedge {B}\in \mathrm{dom}{G}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left(\mathrm{oc}\left({K}\right)\left({x}\right)\in {B}\wedge \mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({x}\right)\right)={x}\wedge \left({x}{\le }_{{K}}{y}\to \mathrm{oc}\left({K}\right)\left({y}\right){\le }_{{K}}\mathrm{oc}\left({K}\right)\left({x}\right)\right)\right)\wedge {x}\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({x}\right)=\mathrm{1.}\left({K}\right)\wedge {x}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({x}\right)=\mathrm{0.}\left({K}\right)\right)\right)$
11 simpl ${⊢}\left(\left({B}\in \mathrm{dom}{U}\wedge {B}\in \mathrm{dom}{G}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left(\mathrm{oc}\left({K}\right)\left({x}\right)\in {B}\wedge \mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({x}\right)\right)={x}\wedge \left({x}{\le }_{{K}}{y}\to \mathrm{oc}\left({K}\right)\left({y}\right){\le }_{{K}}\mathrm{oc}\left({K}\right)\left({x}\right)\right)\right)\wedge {x}\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({x}\right)=\mathrm{1.}\left({K}\right)\wedge {x}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({x}\right)=\mathrm{0.}\left({K}\right)\right)\right)\to \left({B}\in \mathrm{dom}{U}\wedge {B}\in \mathrm{dom}{G}\right)$
12 11 3adantl1 ${⊢}\left(\left({K}\in \mathrm{Poset}\wedge {B}\in \mathrm{dom}{U}\wedge {B}\in \mathrm{dom}{G}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left(\mathrm{oc}\left({K}\right)\left({x}\right)\in {B}\wedge \mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({x}\right)\right)={x}\wedge \left({x}{\le }_{{K}}{y}\to \mathrm{oc}\left({K}\right)\left({y}\right){\le }_{{K}}\mathrm{oc}\left({K}\right)\left({x}\right)\right)\right)\wedge {x}\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({x}\right)=\mathrm{1.}\left({K}\right)\wedge {x}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({x}\right)=\mathrm{0.}\left({K}\right)\right)\right)\to \left({B}\in \mathrm{dom}{U}\wedge {B}\in \mathrm{dom}{G}\right)$
13 10 12 sylbi ${⊢}{K}\in \mathrm{OP}\to \left({B}\in \mathrm{dom}{U}\wedge {B}\in \mathrm{dom}{G}\right)$