# Metamath Proof Explorer

## Theorem glb0N

Description: The greatest lower bound of the empty set is the unit element. (Contributed by NM, 5-Dec-2011) (New usage is discouraged.)

Ref Expression
Hypotheses glb0.g ${⊢}{G}=\mathrm{glb}\left({K}\right)$
glb0.u
Assertion glb0N

### Proof

Step Hyp Ref Expression
1 glb0.g ${⊢}{G}=\mathrm{glb}\left({K}\right)$
2 glb0.u
3 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
4 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
5 biid ${⊢}\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{x}{\le }_{{K}}{y}\wedge \forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{z}{\le }_{{K}}{y}\to {z}{\le }_{{K}}{x}\right)\right)↔\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{x}{\le }_{{K}}{y}\wedge \forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{z}{\le }_{{K}}{y}\to {z}{\le }_{{K}}{x}\right)\right)$
6 id ${⊢}{K}\in \mathrm{OP}\to {K}\in \mathrm{OP}$
7 0ss ${⊢}\varnothing \subseteq {\mathrm{Base}}_{{K}}$
8 7 a1i ${⊢}{K}\in \mathrm{OP}\to \varnothing \subseteq {\mathrm{Base}}_{{K}}$
9 3 4 1 5 6 8 glbval ${⊢}{K}\in \mathrm{OP}\to {G}\left(\varnothing \right)=\left(\iota {x}\in {\mathrm{Base}}_{{K}}|\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{x}{\le }_{{K}}{y}\wedge \forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{z}{\le }_{{K}}{y}\to {z}{\le }_{{K}}{x}\right)\right)\right)$
10 3 2 op1cl
11 ral0 ${⊢}\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{z}{\le }_{{K}}{y}$
12 11 a1bi ${⊢}{z}{\le }_{{K}}{x}↔\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{z}{\le }_{{K}}{y}\to {z}{\le }_{{K}}{x}\right)$
13 12 ralbii ${⊢}\forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}{z}{\le }_{{K}}{x}↔\forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{z}{\le }_{{K}}{y}\to {z}{\le }_{{K}}{x}\right)$
14 ral0 ${⊢}\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{x}{\le }_{{K}}{y}$
15 14 biantrur ${⊢}\forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{z}{\le }_{{K}}{y}\to {z}{\le }_{{K}}{x}\right)↔\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{x}{\le }_{{K}}{y}\wedge \forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{z}{\le }_{{K}}{y}\to {z}{\le }_{{K}}{x}\right)\right)$
16 13 15 bitri ${⊢}\forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}{z}{\le }_{{K}}{x}↔\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{x}{\le }_{{K}}{y}\wedge \forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{z}{\le }_{{K}}{y}\to {z}{\le }_{{K}}{x}\right)\right)$
18 breq1
19 18 rspcv
20 17 19 syl
21 3 4 2 op1le
22 20 21 sylibd
23 3 4 2 ople1