# Metamath Proof Explorer

## Theorem lub0N

Description: The least upper bound of the empty set is the zero element. (Contributed by NM, 15-Sep-2013) (New usage is discouraged.)

Ref Expression
Hypotheses lub0.u
lub0.z
Assertion lub0N

### Proof

Step Hyp Ref Expression
1 lub0.u
2 lub0.z
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}}{y}{\le }_{{K}}{x}\wedge \forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}{\le }_{{K}}{z}\to {x}{\le }_{{K}}{z}\right)\right)↔\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}{\le }_{{K}}{x}\wedge \forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}{\le }_{{K}}{z}\to {x}{\le }_{{K}}{z}\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 lubval
10 3 2 op0cl
11 ral0 ${⊢}\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}{\le }_{{K}}{z}$
12 11 a1bi ${⊢}{x}{\le }_{{K}}{z}↔\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}{\le }_{{K}}{z}\to {x}{\le }_{{K}}{z}\right)$
13 12 ralbii ${⊢}\forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}{x}{\le }_{{K}}{z}↔\forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}{\le }_{{K}}{z}\to {x}{\le }_{{K}}{z}\right)$
14 ral0 ${⊢}\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}{\le }_{{K}}{x}$
15 14 biantrur ${⊢}\forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}{\le }_{{K}}{z}\to {x}{\le }_{{K}}{z}\right)↔\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}{\le }_{{K}}{x}\wedge \forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}{\le }_{{K}}{z}\to {x}{\le }_{{K}}{z}\right)\right)$
16 13 15 bitri ${⊢}\forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}{x}{\le }_{{K}}{z}↔\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}{\le }_{{K}}{x}\wedge \forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{y}{\le }_{{K}}{z}\to {x}{\le }_{{K}}{z}\right)\right)$
18 breq2
19 18 rspcv
20 17 19 syl
21 3 4 2 ople0
22 20 21 sylibd
23 3 4 2 op0le
25 24 ex
26 breq1
27 26 biimprcd
28 25 27 syl6
29 28 com23
30 29 ralrimdv
31 22 30 impbid
32 16 31 bitr3id
33 10 32 riota5
34 9 33 eqtrd