# Metamath Proof Explorer

## Theorem prdsbnd

Description: The product metric over finite index set is bounded if all the factors are bounded. (Contributed by Mario Carneiro, 13-Sep-2015)

Ref Expression
Hypotheses prdsbnd.y ${⊢}{Y}={S}{⨉}_{𝑠}{R}$
prdsbnd.b ${⊢}{B}={\mathrm{Base}}_{{Y}}$
prdsbnd.v ${⊢}{V}={\mathrm{Base}}_{{R}\left({x}\right)}$
prdsbnd.e ${⊢}{E}={\mathrm{dist}\left({R}\left({x}\right)\right)↾}_{\left({V}×{V}\right)}$
prdsbnd.d ${⊢}{D}=\mathrm{dist}\left({Y}\right)$
prdsbnd.s ${⊢}{\phi }\to {S}\in {W}$
prdsbnd.i ${⊢}{\phi }\to {I}\in \mathrm{Fin}$
prdsbnd.r ${⊢}{\phi }\to {R}Fn{I}$
prdsbnd.m ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {E}\in \mathrm{Bnd}\left({V}\right)$
Assertion prdsbnd ${⊢}{\phi }\to {D}\in \mathrm{Bnd}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 prdsbnd.y ${⊢}{Y}={S}{⨉}_{𝑠}{R}$
2 prdsbnd.b ${⊢}{B}={\mathrm{Base}}_{{Y}}$
3 prdsbnd.v ${⊢}{V}={\mathrm{Base}}_{{R}\left({x}\right)}$
4 prdsbnd.e ${⊢}{E}={\mathrm{dist}\left({R}\left({x}\right)\right)↾}_{\left({V}×{V}\right)}$
5 prdsbnd.d ${⊢}{D}=\mathrm{dist}\left({Y}\right)$
6 prdsbnd.s ${⊢}{\phi }\to {S}\in {W}$
7 prdsbnd.i ${⊢}{\phi }\to {I}\in \mathrm{Fin}$
8 prdsbnd.r ${⊢}{\phi }\to {R}Fn{I}$
9 prdsbnd.m ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {E}\in \mathrm{Bnd}\left({V}\right)$
10 eqid ${⊢}{S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)={S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)$
11 eqid ${⊢}{\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)}={\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)}$
12 eqid ${⊢}\mathrm{dist}\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)=\mathrm{dist}\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)$
13 fvexd ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {R}\left({x}\right)\in \mathrm{V}$
14 bndmet ${⊢}{E}\in \mathrm{Bnd}\left({V}\right)\to {E}\in \mathrm{Met}\left({V}\right)$
15 9 14 syl ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to {E}\in \mathrm{Met}\left({V}\right)$
16 10 11 3 4 12 6 7 13 15 prdsmet ${⊢}{\phi }\to \mathrm{dist}\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)\in \mathrm{Met}\left({\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)}\right)$
17 dffn5 ${⊢}{R}Fn{I}↔{R}=\left({x}\in {I}⟼{R}\left({x}\right)\right)$
18 8 17 sylib ${⊢}{\phi }\to {R}=\left({x}\in {I}⟼{R}\left({x}\right)\right)$
19 18 oveq2d ${⊢}{\phi }\to {S}{⨉}_{𝑠}{R}={S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)$
20 1 19 syl5eq ${⊢}{\phi }\to {Y}={S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)$
21 20 fveq2d ${⊢}{\phi }\to \mathrm{dist}\left({Y}\right)=\mathrm{dist}\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)$
22 5 21 syl5eq ${⊢}{\phi }\to {D}=\mathrm{dist}\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)$
23 20 fveq2d ${⊢}{\phi }\to {\mathrm{Base}}_{{Y}}={\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)}$
24 2 23 syl5eq ${⊢}{\phi }\to {B}={\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)}$
25 24 fveq2d ${⊢}{\phi }\to \mathrm{Met}\left({B}\right)=\mathrm{Met}\left({\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)}\right)$
26 16 22 25 3eltr4d ${⊢}{\phi }\to {D}\in \mathrm{Met}\left({B}\right)$
27 isbnd3 ${⊢}{E}\in \mathrm{Bnd}\left({V}\right)↔\left({E}\in \mathrm{Met}\left({V}\right)\wedge \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{w}\right]\right)$
28 27 simprbi ${⊢}{E}\in \mathrm{Bnd}\left({V}\right)\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{w}\right]$
29 9 28 syl ${⊢}\left({\phi }\wedge {x}\in {I}\right)\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{w}\right]$
30 29 ralrimiva ${⊢}{\phi }\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{w}\right]$
31 oveq2 ${⊢}{w}={k}\left({x}\right)\to \left[0,{w}\right]=\left[0,{k}\left({x}\right)\right]$
32 31 feq3d ${⊢}{w}={k}\left({x}\right)\to \left({E}:{V}×{V}⟶\left[0,{w}\right]↔{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)$
33 32 ac6sfi ${⊢}\left({I}\in \mathrm{Fin}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{w}\right]\right)\to \exists {k}\phantom{\rule{.4em}{0ex}}\left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)$
34 7 30 33 syl2anc ${⊢}{\phi }\to \exists {k}\phantom{\rule{.4em}{0ex}}\left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)$
35 frn ${⊢}{k}:{I}⟶ℝ\to \mathrm{ran}{k}\subseteq ℝ$
36 35 adantl ${⊢}\left({\phi }\wedge {k}:{I}⟶ℝ\right)\to \mathrm{ran}{k}\subseteq ℝ$
37 0red ${⊢}{\phi }\to 0\in ℝ$
38 37 snssd ${⊢}{\phi }\to \left\{0\right\}\subseteq ℝ$
39 38 adantr ${⊢}\left({\phi }\wedge {k}:{I}⟶ℝ\right)\to \left\{0\right\}\subseteq ℝ$
40 36 39 unssd ${⊢}\left({\phi }\wedge {k}:{I}⟶ℝ\right)\to \mathrm{ran}{k}\cup \left\{0\right\}\subseteq ℝ$
41 ffn ${⊢}{k}:{I}⟶ℝ\to {k}Fn{I}$
42 dffn4 ${⊢}{k}Fn{I}↔{k}:{I}\underset{onto}{⟶}\mathrm{ran}{k}$
43 41 42 sylib ${⊢}{k}:{I}⟶ℝ\to {k}:{I}\underset{onto}{⟶}\mathrm{ran}{k}$
44 fofi ${⊢}\left({I}\in \mathrm{Fin}\wedge {k}:{I}\underset{onto}{⟶}\mathrm{ran}{k}\right)\to \mathrm{ran}{k}\in \mathrm{Fin}$
45 7 43 44 syl2an ${⊢}\left({\phi }\wedge {k}:{I}⟶ℝ\right)\to \mathrm{ran}{k}\in \mathrm{Fin}$
46 snfi ${⊢}\left\{0\right\}\in \mathrm{Fin}$
47 unfi ${⊢}\left(\mathrm{ran}{k}\in \mathrm{Fin}\wedge \left\{0\right\}\in \mathrm{Fin}\right)\to \mathrm{ran}{k}\cup \left\{0\right\}\in \mathrm{Fin}$
48 45 46 47 sylancl ${⊢}\left({\phi }\wedge {k}:{I}⟶ℝ\right)\to \mathrm{ran}{k}\cup \left\{0\right\}\in \mathrm{Fin}$
49 ssun2 ${⊢}\left\{0\right\}\subseteq \mathrm{ran}{k}\cup \left\{0\right\}$
50 c0ex ${⊢}0\in \mathrm{V}$
51 50 snid ${⊢}0\in \left\{0\right\}$
52 49 51 sselii ${⊢}0\in \left(\mathrm{ran}{k}\cup \left\{0\right\}\right)$
53 ne0i ${⊢}0\in \left(\mathrm{ran}{k}\cup \left\{0\right\}\right)\to \mathrm{ran}{k}\cup \left\{0\right\}\ne \varnothing$
54 52 53 mp1i ${⊢}\left({\phi }\wedge {k}:{I}⟶ℝ\right)\to \mathrm{ran}{k}\cup \left\{0\right\}\ne \varnothing$
55 ltso ${⊢}<\mathrm{Or}ℝ$
56 fisupcl ${⊢}\left(<\mathrm{Or}ℝ\wedge \left(\mathrm{ran}{k}\cup \left\{0\right\}\in \mathrm{Fin}\wedge \mathrm{ran}{k}\cup \left\{0\right\}\ne \varnothing \wedge \mathrm{ran}{k}\cup \left\{0\right\}\subseteq ℝ\right)\right)\to sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\in \left(\mathrm{ran}{k}\cup \left\{0\right\}\right)$
57 55 56 mpan ${⊢}\left(\mathrm{ran}{k}\cup \left\{0\right\}\in \mathrm{Fin}\wedge \mathrm{ran}{k}\cup \left\{0\right\}\ne \varnothing \wedge \mathrm{ran}{k}\cup \left\{0\right\}\subseteq ℝ\right)\to sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\in \left(\mathrm{ran}{k}\cup \left\{0\right\}\right)$
58 48 54 40 57 syl3anc ${⊢}\left({\phi }\wedge {k}:{I}⟶ℝ\right)\to sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\in \left(\mathrm{ran}{k}\cup \left\{0\right\}\right)$
59 40 58 sseldd ${⊢}\left({\phi }\wedge {k}:{I}⟶ℝ\right)\to sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\in ℝ$
60 59 adantrr ${⊢}\left({\phi }\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\in ℝ$
61 metf ${⊢}{D}\in \mathrm{Met}\left({B}\right)\to {D}:{B}×{B}⟶ℝ$
62 ffn ${⊢}{D}:{B}×{B}⟶ℝ\to {D}Fn\left({B}×{B}\right)$
63 26 61 62 3syl ${⊢}{\phi }\to {D}Fn\left({B}×{B}\right)$
64 63 adantr ${⊢}\left({\phi }\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to {D}Fn\left({B}×{B}\right)$
65 26 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to {D}\in \mathrm{Met}\left({B}\right)$
66 simprl ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to {f}\in {B}$
67 66 adantr ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to {f}\in {B}$
68 simprr ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to {g}\in {B}$
69 68 adantr ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to {g}\in {B}$
70 metcl ${⊢}\left({D}\in \mathrm{Met}\left({B}\right)\wedge {f}\in {B}\wedge {g}\in {B}\right)\to {f}{D}{g}\in ℝ$
71 65 67 69 70 syl3anc ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to {f}{D}{g}\in ℝ$
72 metge0 ${⊢}\left({D}\in \mathrm{Met}\left({B}\right)\wedge {f}\in {B}\wedge {g}\in {B}\right)\to 0\le {f}{D}{g}$
73 65 67 69 72 syl3anc ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to 0\le {f}{D}{g}$
74 22 oveqdr ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to {f}{D}{g}={f}\mathrm{dist}\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right){g}$
75 6 adantr ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to {S}\in {W}$
76 7 adantr ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to {I}\in \mathrm{Fin}$
77 fvexd ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {x}\in {I}\right)\to {R}\left({x}\right)\in \mathrm{V}$
78 77 ralrimiva ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{R}\left({x}\right)\in \mathrm{V}$
79 24 adantr ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to {B}={\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)}$
80 66 79 eleqtrd ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to {f}\in {\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)}$
81 68 79 eleqtrd ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to {g}\in {\mathrm{Base}}_{\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right)}$
82 10 11 75 76 78 80 81 3 4 12 prdsdsval3 ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to {f}\mathrm{dist}\left({S}{⨉}_{𝑠}\left({x}\in {I}⟼{R}\left({x}\right)\right)\right){g}=sup\left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)$
83 74 82 eqtrd ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to {f}{D}{g}=sup\left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)$
84 83 adantr ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to {f}{D}{g}=sup\left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)$
85 15 adantlr ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {x}\in {I}\right)\to {E}\in \mathrm{Met}\left({V}\right)$
86 10 11 75 76 78 3 80 prdsbascl ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {V}$
87 86 r19.21bi ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {x}\in {I}\right)\to {f}\left({x}\right)\in {V}$
88 10 11 75 76 78 3 81 prdsbascl ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {V}$
89 88 r19.21bi ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {x}\in {I}\right)\to {g}\left({x}\right)\in {V}$
90 metcl ${⊢}\left({E}\in \mathrm{Met}\left({V}\right)\wedge {f}\left({x}\right)\in {V}\wedge {g}\left({x}\right)\in {V}\right)\to {f}\left({x}\right){E}{g}\left({x}\right)\in ℝ$
91 85 87 89 90 syl3anc ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {x}\in {I}\right)\to {f}\left({x}\right){E}{g}\left({x}\right)\in ℝ$
92 91 ad2ant2r ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\wedge \left({x}\in {I}\wedge {E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to {f}\left({x}\right){E}{g}\left({x}\right)\in ℝ$
93 ffvelrn ${⊢}\left({k}:{I}⟶ℝ\wedge {x}\in {I}\right)\to {k}\left({x}\right)\in ℝ$
94 93 ad2ant2lr ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\wedge \left({x}\in {I}\wedge {E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to {k}\left({x}\right)\in ℝ$
95 59 adantlr ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\to sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\in ℝ$
96 95 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\wedge \left({x}\in {I}\wedge {E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\in ℝ$
97 simprr ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\wedge \left({x}\in {I}\wedge {E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to {E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]$
98 87 ad2ant2r ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\wedge \left({x}\in {I}\wedge {E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to {f}\left({x}\right)\in {V}$
99 89 ad2ant2r ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\wedge \left({x}\in {I}\wedge {E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to {g}\left({x}\right)\in {V}$
100 97 98 99 fovrnd ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\wedge \left({x}\in {I}\wedge {E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to {f}\left({x}\right){E}{g}\left({x}\right)\in \left[0,{k}\left({x}\right)\right]$
101 0re ${⊢}0\in ℝ$
102 elicc2 ${⊢}\left(0\in ℝ\wedge {k}\left({x}\right)\in ℝ\right)\to \left({f}\left({x}\right){E}{g}\left({x}\right)\in \left[0,{k}\left({x}\right)\right]↔\left({f}\left({x}\right){E}{g}\left({x}\right)\in ℝ\wedge 0\le {f}\left({x}\right){E}{g}\left({x}\right)\wedge {f}\left({x}\right){E}{g}\left({x}\right)\le {k}\left({x}\right)\right)\right)$
103 101 94 102 sylancr ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\wedge \left({x}\in {I}\wedge {E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to \left({f}\left({x}\right){E}{g}\left({x}\right)\in \left[0,{k}\left({x}\right)\right]↔\left({f}\left({x}\right){E}{g}\left({x}\right)\in ℝ\wedge 0\le {f}\left({x}\right){E}{g}\left({x}\right)\wedge {f}\left({x}\right){E}{g}\left({x}\right)\le {k}\left({x}\right)\right)\right)$
104 100 103 mpbid ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\wedge \left({x}\in {I}\wedge {E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to \left({f}\left({x}\right){E}{g}\left({x}\right)\in ℝ\wedge 0\le {f}\left({x}\right){E}{g}\left({x}\right)\wedge {f}\left({x}\right){E}{g}\left({x}\right)\le {k}\left({x}\right)\right)$
105 104 simp3d ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\wedge \left({x}\in {I}\wedge {E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to {f}\left({x}\right){E}{g}\left({x}\right)\le {k}\left({x}\right)$
106 40 adantlr ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\to \mathrm{ran}{k}\cup \left\{0\right\}\subseteq ℝ$
107 106 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\wedge \left({x}\in {I}\wedge {E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to \mathrm{ran}{k}\cup \left\{0\right\}\subseteq ℝ$
108 52 53 mp1i ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\wedge \left({x}\in {I}\wedge {E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to \mathrm{ran}{k}\cup \left\{0\right\}\ne \varnothing$
109 fimaxre2 ${⊢}\left(\mathrm{ran}{k}\cup \left\{0\right\}\subseteq ℝ\wedge \mathrm{ran}{k}\cup \left\{0\right\}\in \mathrm{Fin}\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in \left(\mathrm{ran}{k}\cup \left\{0\right\}\right)\phantom{\rule{.4em}{0ex}}{w}\le {z}$
110 40 48 109 syl2anc ${⊢}\left({\phi }\wedge {k}:{I}⟶ℝ\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in \left(\mathrm{ran}{k}\cup \left\{0\right\}\right)\phantom{\rule{.4em}{0ex}}{w}\le {z}$
111 110 adantlr ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in \left(\mathrm{ran}{k}\cup \left\{0\right\}\right)\phantom{\rule{.4em}{0ex}}{w}\le {z}$
112 111 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\wedge \left({x}\in {I}\wedge {E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in \left(\mathrm{ran}{k}\cup \left\{0\right\}\right)\phantom{\rule{.4em}{0ex}}{w}\le {z}$
113 ssun1 ${⊢}\mathrm{ran}{k}\subseteq \mathrm{ran}{k}\cup \left\{0\right\}$
114 41 ad2antlr ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\wedge \left({x}\in {I}\wedge {E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to {k}Fn{I}$
115 simprl ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\wedge \left({x}\in {I}\wedge {E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to {x}\in {I}$
116 fnfvelrn ${⊢}\left({k}Fn{I}\wedge {x}\in {I}\right)\to {k}\left({x}\right)\in \mathrm{ran}{k}$
117 114 115 116 syl2anc ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\wedge \left({x}\in {I}\wedge {E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to {k}\left({x}\right)\in \mathrm{ran}{k}$
118 113 117 sseldi ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\wedge \left({x}\in {I}\wedge {E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to {k}\left({x}\right)\in \left(\mathrm{ran}{k}\cup \left\{0\right\}\right)$
119 suprub ${⊢}\left(\left(\mathrm{ran}{k}\cup \left\{0\right\}\subseteq ℝ\wedge \mathrm{ran}{k}\cup \left\{0\right\}\ne \varnothing \wedge \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in \left(\mathrm{ran}{k}\cup \left\{0\right\}\right)\phantom{\rule{.4em}{0ex}}{w}\le {z}\right)\wedge {k}\left({x}\right)\in \left(\mathrm{ran}{k}\cup \left\{0\right\}\right)\right)\to {k}\left({x}\right)\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)$
120 107 108 112 118 119 syl31anc ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\wedge \left({x}\in {I}\wedge {E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to {k}\left({x}\right)\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)$
121 92 94 96 105 120 letrd ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\wedge \left({x}\in {I}\wedge {E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to {f}\left({x}\right){E}{g}\left({x}\right)\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)$
122 121 expr ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\wedge {x}\in {I}\right)\to \left({E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\to {f}\left({x}\right){E}{g}\left({x}\right)\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\right)$
123 122 ralimdva ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge {k}:{I}⟶ℝ\right)\to \left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){E}{g}\left({x}\right)\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\right)$
124 123 impr ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){E}{g}\left({x}\right)\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)$
125 ovex ${⊢}{f}\left({x}\right){E}{g}\left({x}\right)\in \mathrm{V}$
126 125 rgenw ${⊢}\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){E}{g}\left({x}\right)\in \mathrm{V}$
127 eqid ${⊢}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)=\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)$
128 breq1 ${⊢}{w}={f}\left({x}\right){E}{g}\left({x}\right)\to \left({w}\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)↔{f}\left({x}\right){E}{g}\left({x}\right)\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\right)$
129 127 128 ralrnmptw ${⊢}\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){E}{g}\left({x}\right)\in \mathrm{V}\to \left(\forall {w}\in \mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\phantom{\rule{.4em}{0ex}}{w}\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)↔\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){E}{g}\left({x}\right)\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\right)$
130 126 129 ax-mp ${⊢}\forall {w}\in \mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\phantom{\rule{.4em}{0ex}}{w}\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)↔\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){E}{g}\left({x}\right)\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)$
131 124 130 sylibr ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to \forall {w}\in \mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\phantom{\rule{.4em}{0ex}}{w}\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)$
132 40 ad2ant2r ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to \mathrm{ran}{k}\cup \left\{0\right\}\subseteq ℝ$
133 52 53 mp1i ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to \mathrm{ran}{k}\cup \left\{0\right\}\ne \varnothing$
134 110 ad2ant2r ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in \left(\mathrm{ran}{k}\cup \left\{0\right\}\right)\phantom{\rule{.4em}{0ex}}{w}\le {z}$
135 52 a1i ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to 0\in \left(\mathrm{ran}{k}\cup \left\{0\right\}\right)$
136 suprub ${⊢}\left(\left(\mathrm{ran}{k}\cup \left\{0\right\}\subseteq ℝ\wedge \mathrm{ran}{k}\cup \left\{0\right\}\ne \varnothing \wedge \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in \left(\mathrm{ran}{k}\cup \left\{0\right\}\right)\phantom{\rule{.4em}{0ex}}{w}\le {z}\right)\wedge 0\in \left(\mathrm{ran}{k}\cup \left\{0\right\}\right)\right)\to 0\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)$
137 132 133 134 135 136 syl31anc ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to 0\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)$
138 elsni ${⊢}{w}\in \left\{0\right\}\to {w}=0$
139 138 breq1d ${⊢}{w}\in \left\{0\right\}\to \left({w}\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)↔0\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\right)$
140 137 139 syl5ibrcom ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to \left({w}\in \left\{0\right\}\to {w}\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\right)$
141 140 ralrimiv ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to \forall {w}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}{w}\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)$
142 ralunb ${⊢}\forall {w}\in \left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}\right)\phantom{\rule{.4em}{0ex}}{w}\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)↔\left(\forall {w}\in \mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\phantom{\rule{.4em}{0ex}}{w}\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\wedge \forall {w}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}{w}\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\right)$
143 131 141 142 sylanbrc ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to \forall {w}\in \left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}\right)\phantom{\rule{.4em}{0ex}}{w}\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)$
144 91 fmpttd ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to \left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right):{I}⟶ℝ$
145 144 frnd ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to \mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\subseteq ℝ$
146 0red ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to 0\in ℝ$
147 146 snssd ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to \left\{0\right\}\subseteq ℝ$
148 145 147 unssd ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to \mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}\subseteq ℝ$
149 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
150 148 149 sstrdi ${⊢}\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to \mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}\subseteq {ℝ}^{*}$
151 150 adantr ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to \mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}\subseteq {ℝ}^{*}$
152 60 adantlr ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\in ℝ$
153 152 rexrd ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\in {ℝ}^{*}$
154 supxrleub ${⊢}\left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}\subseteq {ℝ}^{*}\wedge sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\in {ℝ}^{*}\right)\to \left(sup\left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)↔\forall {w}\in \left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}\right)\phantom{\rule{.4em}{0ex}}{w}\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\right)$
155 151 153 154 syl2anc ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to \left(sup\left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)↔\forall {w}\in \left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\}\right)\phantom{\rule{.4em}{0ex}}{w}\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\right)$
156 143 155 mpbird ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to sup\left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right){E}{g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)$
157 84 156 eqbrtrd ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to {f}{D}{g}\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)$
158 elicc2 ${⊢}\left(0\in ℝ\wedge sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\in ℝ\right)\to \left({f}{D}{g}\in \left[0,sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\right]↔\left({f}{D}{g}\in ℝ\wedge 0\le {f}{D}{g}\wedge {f}{D}{g}\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\right)\right)$
159 101 152 158 sylancr ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to \left({f}{D}{g}\in \left[0,sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\right]↔\left({f}{D}{g}\in ℝ\wedge 0\le {f}{D}{g}\wedge {f}{D}{g}\le sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\right)\right)$
160 71 73 157 159 mpbir3and ${⊢}\left(\left({\phi }\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to {f}{D}{g}\in \left[0,sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\right]$
161 160 an32s ${⊢}\left(\left({\phi }\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\wedge \left({f}\in {B}\wedge {g}\in {B}\right)\right)\to {f}{D}{g}\in \left[0,sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\right]$
162 161 ralrimivva ${⊢}\left({\phi }\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to \forall {f}\in {B}\phantom{\rule{.4em}{0ex}}\forall {g}\in {B}\phantom{\rule{.4em}{0ex}}{f}{D}{g}\in \left[0,sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\right]$
163 ffnov ${⊢}{D}:{B}×{B}⟶\left[0,sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\right]↔\left({D}Fn\left({B}×{B}\right)\wedge \forall {f}\in {B}\phantom{\rule{.4em}{0ex}}\forall {g}\in {B}\phantom{\rule{.4em}{0ex}}{f}{D}{g}\in \left[0,sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\right]\right)$
164 64 162 163 sylanbrc ${⊢}\left({\phi }\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to {D}:{B}×{B}⟶\left[0,sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\right]$
165 oveq2 ${⊢}{m}=sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\to \left[0,{m}\right]=\left[0,sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\right]$
166 165 feq3d ${⊢}{m}=sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\to \left({D}:{B}×{B}⟶\left[0,{m}\right]↔{D}:{B}×{B}⟶\left[0,sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\right]\right)$
167 166 rspcev ${⊢}\left(sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\in ℝ\wedge {D}:{B}×{B}⟶\left[0,sup\left(\mathrm{ran}{k}\cup \left\{0\right\},ℝ,<\right)\right]\right)\to \exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}{D}:{B}×{B}⟶\left[0,{m}\right]$
168 60 164 167 syl2anc ${⊢}\left({\phi }\wedge \left({k}:{I}⟶ℝ\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{E}:{V}×{V}⟶\left[0,{k}\left({x}\right)\right]\right)\right)\to \exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}{D}:{B}×{B}⟶\left[0,{m}\right]$
169 34 168 exlimddv ${⊢}{\phi }\to \exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}{D}:{B}×{B}⟶\left[0,{m}\right]$
170 isbnd3 ${⊢}{D}\in \mathrm{Bnd}\left({B}\right)↔\left({D}\in \mathrm{Met}\left({B}\right)\wedge \exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}{D}:{B}×{B}⟶\left[0,{m}\right]\right)$
171 26 169 170 sylanbrc ${⊢}{\phi }\to {D}\in \mathrm{Bnd}\left({B}\right)$