# Metamath Proof Explorer

## Theorem xlebnum

Description: Generalize lebnum to extended metrics. (Contributed by Mario Carneiro, 5-Sep-2015)

Ref Expression
Hypotheses xlebnum.j ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
xlebnum.d ${⊢}{\phi }\to {D}\in \mathrm{\infty Met}\left({X}\right)$
xlebnum.c ${⊢}{\phi }\to {J}\in \mathrm{Comp}$
xlebnum.s ${⊢}{\phi }\to {U}\subseteq {J}$
xlebnum.u ${⊢}{\phi }\to {X}=\bigcup {U}$
Assertion xlebnum ${⊢}{\phi }\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right){d}\subseteq {u}$

### Proof

Step Hyp Ref Expression
1 xlebnum.j ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
2 xlebnum.d ${⊢}{\phi }\to {D}\in \mathrm{\infty Met}\left({X}\right)$
3 xlebnum.c ${⊢}{\phi }\to {J}\in \mathrm{Comp}$
4 xlebnum.s ${⊢}{\phi }\to {U}\subseteq {J}$
5 xlebnum.u ${⊢}{\phi }\to {X}=\bigcup {U}$
6 eqid ${⊢}\mathrm{MetOpen}\left(\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\right)=\mathrm{MetOpen}\left(\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\right)$
7 1rp ${⊢}1\in {ℝ}^{+}$
8 eqid ${⊢}\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)=\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)$
9 8 stdbdmet ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge 1\in {ℝ}^{+}\right)\to \left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\in \mathrm{Met}\left({X}\right)$
10 2 7 9 sylancl ${⊢}{\phi }\to \left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\in \mathrm{Met}\left({X}\right)$
11 rpxr ${⊢}1\in {ℝ}^{+}\to 1\in {ℝ}^{*}$
12 7 11 mp1i ${⊢}{\phi }\to 1\in {ℝ}^{*}$
13 0lt1 ${⊢}0<1$
14 13 a1i ${⊢}{\phi }\to 0<1$
15 8 1 stdbdmopn ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge 1\in {ℝ}^{*}\wedge 0<1\right)\to {J}=\mathrm{MetOpen}\left(\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\right)$
16 2 12 14 15 syl3anc ${⊢}{\phi }\to {J}=\mathrm{MetOpen}\left(\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\right)$
17 16 3 eqeltrrd ${⊢}{\phi }\to \mathrm{MetOpen}\left(\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\right)\in \mathrm{Comp}$
18 4 16 sseqtrd ${⊢}{\phi }\to {U}\subseteq \mathrm{MetOpen}\left(\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\right)$
19 6 10 17 18 5 lebnum ${⊢}{\phi }\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left(\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\right){r}\subseteq {u}$
20 simpr ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to {r}\in {ℝ}^{+}$
21 ifcl ${⊢}\left({r}\in {ℝ}^{+}\wedge 1\in {ℝ}^{+}\right)\to if\left({r}\le 1,{r},1\right)\in {ℝ}^{+}$
22 20 7 21 sylancl ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to if\left({r}\le 1,{r},1\right)\in {ℝ}^{+}$
23 2 ad2antrr ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$
24 7 11 mp1i ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to 1\in {ℝ}^{*}$
25 13 a1i ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to 0<1$
26 simpr ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to {x}\in {X}$
27 22 adantr ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to if\left({r}\le 1,{r},1\right)\in {ℝ}^{+}$
28 rpxr ${⊢}if\left({r}\le 1,{r},1\right)\in {ℝ}^{+}\to if\left({r}\le 1,{r},1\right)\in {ℝ}^{*}$
29 27 28 syl ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to if\left({r}\le 1,{r},1\right)\in {ℝ}^{*}$
30 rpre ${⊢}{r}\in {ℝ}^{+}\to {r}\in ℝ$
31 30 ad2antlr ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to {r}\in ℝ$
32 1re ${⊢}1\in ℝ$
33 min2 ${⊢}\left({r}\in ℝ\wedge 1\in ℝ\right)\to if\left({r}\le 1,{r},1\right)\le 1$
34 31 32 33 sylancl ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to if\left({r}\le 1,{r},1\right)\le 1$
35 8 stdbdbl ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge 1\in {ℝ}^{*}\wedge 0<1\right)\wedge \left({x}\in {X}\wedge if\left({r}\le 1,{r},1\right)\in {ℝ}^{*}\wedge if\left({r}\le 1,{r},1\right)\le 1\right)\right)\to {x}\mathrm{ball}\left(\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\right)if\left({r}\le 1,{r},1\right)={x}\mathrm{ball}\left({D}\right)if\left({r}\le 1,{r},1\right)$
36 23 24 25 26 29 34 35 syl33anc ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to {x}\mathrm{ball}\left(\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\right)if\left({r}\le 1,{r},1\right)={x}\mathrm{ball}\left({D}\right)if\left({r}\le 1,{r},1\right)$
37 10 ad2antrr ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to \left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\in \mathrm{Met}\left({X}\right)$
38 metxmet ${⊢}\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\in \mathrm{Met}\left({X}\right)\to \left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\in \mathrm{\infty Met}\left({X}\right)$
39 37 38 syl ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to \left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\in \mathrm{\infty Met}\left({X}\right)$
40 rpxr ${⊢}{r}\in {ℝ}^{+}\to {r}\in {ℝ}^{*}$
41 40 ad2antlr ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to {r}\in {ℝ}^{*}$
42 min1 ${⊢}\left({r}\in ℝ\wedge 1\in ℝ\right)\to if\left({r}\le 1,{r},1\right)\le {r}$
43 31 32 42 sylancl ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to if\left({r}\le 1,{r},1\right)\le {r}$
44 ssbl ${⊢}\left(\left(\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\right)\wedge \left(if\left({r}\le 1,{r},1\right)\in {ℝ}^{*}\wedge {r}\in {ℝ}^{*}\right)\wedge if\left({r}\le 1,{r},1\right)\le {r}\right)\to {x}\mathrm{ball}\left(\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\right)if\left({r}\le 1,{r},1\right)\subseteq {x}\mathrm{ball}\left(\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\right){r}$
45 39 26 29 41 43 44 syl221anc ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to {x}\mathrm{ball}\left(\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\right)if\left({r}\le 1,{r},1\right)\subseteq {x}\mathrm{ball}\left(\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\right){r}$
46 36 45 eqsstrrd ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to {x}\mathrm{ball}\left({D}\right)if\left({r}\le 1,{r},1\right)\subseteq {x}\mathrm{ball}\left(\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\right){r}$
47 sstr2 ${⊢}{x}\mathrm{ball}\left({D}\right)if\left({r}\le 1,{r},1\right)\subseteq {x}\mathrm{ball}\left(\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\right){r}\to \left({x}\mathrm{ball}\left(\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\right){r}\subseteq {u}\to {x}\mathrm{ball}\left({D}\right)if\left({r}\le 1,{r},1\right)\subseteq {u}\right)$
48 46 47 syl ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to \left({x}\mathrm{ball}\left(\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\right){r}\subseteq {u}\to {x}\mathrm{ball}\left({D}\right)if\left({r}\le 1,{r},1\right)\subseteq {u}\right)$
49 48 reximdv ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to \left(\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left(\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\right){r}\subseteq {u}\to \exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right)if\left({r}\le 1,{r},1\right)\subseteq {u}\right)$
50 49 ralimdva ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left(\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\right){r}\subseteq {u}\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right)if\left({r}\le 1,{r},1\right)\subseteq {u}\right)$
51 oveq2 ${⊢}{d}=if\left({r}\le 1,{r},1\right)\to {x}\mathrm{ball}\left({D}\right){d}={x}\mathrm{ball}\left({D}\right)if\left({r}\le 1,{r},1\right)$
52 51 sseq1d ${⊢}{d}=if\left({r}\le 1,{r},1\right)\to \left({x}\mathrm{ball}\left({D}\right){d}\subseteq {u}↔{x}\mathrm{ball}\left({D}\right)if\left({r}\le 1,{r},1\right)\subseteq {u}\right)$
53 52 rexbidv ${⊢}{d}=if\left({r}\le 1,{r},1\right)\to \left(\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right){d}\subseteq {u}↔\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right)if\left({r}\le 1,{r},1\right)\subseteq {u}\right)$
54 53 ralbidv ${⊢}{d}=if\left({r}\le 1,{r},1\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right){d}\subseteq {u}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right)if\left({r}\le 1,{r},1\right)\subseteq {u}\right)$
55 54 rspcev ${⊢}\left(if\left({r}\le 1,{r},1\right)\in {ℝ}^{+}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right)if\left({r}\le 1,{r},1\right)\subseteq {u}\right)\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right){d}\subseteq {u}$
56 22 50 55 syl6an ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left(\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\right){r}\subseteq {u}\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right){d}\subseteq {u}\right)$
57 56 rexlimdva ${⊢}{\phi }\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left(\left({y}\in {X},{z}\in {X}⟼if\left({y}{D}{z}\le 1,{y}{D}{z},1\right)\right)\right){r}\subseteq {u}\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right){d}\subseteq {u}\right)$
58 19 57 mpd ${⊢}{\phi }\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right){d}\subseteq {u}$