# Metamath Proof Explorer

## Theorem metucn

Description: Uniform continuity in metric spaces. Compare the order of the quantifiers with metcn . (Contributed by Thierry Arnoux, 26-Jan-2018) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Hypotheses metucn.u ${⊢}{U}=\mathrm{metUnif}\left({C}\right)$
metucn.v ${⊢}{V}=\mathrm{metUnif}\left({D}\right)$
metucn.x ${⊢}{\phi }\to {X}\ne \varnothing$
metucn.y ${⊢}{\phi }\to {Y}\ne \varnothing$
metucn.c ${⊢}{\phi }\to {C}\in \mathrm{PsMet}\left({X}\right)$
metucn.d ${⊢}{\phi }\to {D}\in \mathrm{PsMet}\left({Y}\right)$
Assertion metucn ${⊢}{\phi }\to \left({F}\in \left({U}\mathrm{uCn}{V}\right)↔\left({F}:{X}⟶{Y}\wedge \forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{C}{y}<{c}\to {F}\left({x}\right){D}{F}\left({y}\right)<{d}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 metucn.u ${⊢}{U}=\mathrm{metUnif}\left({C}\right)$
2 metucn.v ${⊢}{V}=\mathrm{metUnif}\left({D}\right)$
3 metucn.x ${⊢}{\phi }\to {X}\ne \varnothing$
4 metucn.y ${⊢}{\phi }\to {Y}\ne \varnothing$
5 metucn.c ${⊢}{\phi }\to {C}\in \mathrm{PsMet}\left({X}\right)$
6 metucn.d ${⊢}{\phi }\to {D}\in \mathrm{PsMet}\left({Y}\right)$
7 metuval ${⊢}{C}\in \mathrm{PsMet}\left({X}\right)\to \mathrm{metUnif}\left({C}\right)=\left({X}×{X}\right)\mathrm{filGen}\mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)$
8 5 7 syl ${⊢}{\phi }\to \mathrm{metUnif}\left({C}\right)=\left({X}×{X}\right)\mathrm{filGen}\mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)$
9 1 8 syl5eq ${⊢}{\phi }\to {U}=\left({X}×{X}\right)\mathrm{filGen}\mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)$
10 metuval ${⊢}{D}\in \mathrm{PsMet}\left({Y}\right)\to \mathrm{metUnif}\left({D}\right)=\left({Y}×{Y}\right)\mathrm{filGen}\mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)$
11 6 10 syl ${⊢}{\phi }\to \mathrm{metUnif}\left({D}\right)=\left({Y}×{Y}\right)\mathrm{filGen}\mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)$
12 2 11 syl5eq ${⊢}{\phi }\to {V}=\left({Y}×{Y}\right)\mathrm{filGen}\mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)$
13 9 12 oveq12d ${⊢}{\phi }\to {U}\mathrm{uCn}{V}=\left(\left({X}×{X}\right)\mathrm{filGen}\mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)\right)\mathrm{uCn}\left(\left({Y}×{Y}\right)\mathrm{filGen}\mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)\right)$
14 13 eleq2d ${⊢}{\phi }\to \left({F}\in \left({U}\mathrm{uCn}{V}\right)↔{F}\in \left(\left(\left({X}×{X}\right)\mathrm{filGen}\mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)\right)\mathrm{uCn}\left(\left({Y}×{Y}\right)\mathrm{filGen}\mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)\right)\right)\right)$
15 eqid ${⊢}\left({X}×{X}\right)\mathrm{filGen}\mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)=\left({X}×{X}\right)\mathrm{filGen}\mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)$
16 eqid ${⊢}\left({Y}×{Y}\right)\mathrm{filGen}\mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)=\left({Y}×{Y}\right)\mathrm{filGen}\mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)$
17 oveq2 ${⊢}{a}={c}\to \left[0,{a}\right)=\left[0,{c}\right)$
18 17 imaeq2d ${⊢}{a}={c}\to {{C}}^{-1}\left[\left[0,{a}\right)\right]={{C}}^{-1}\left[\left[0,{c}\right)\right]$
19 18 cbvmptv ${⊢}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)=\left({c}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{c}\right)\right]\right)$
20 19 rneqi ${⊢}\mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)=\mathrm{ran}\left({c}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{c}\right)\right]\right)$
21 20 metust ${⊢}\left({X}\ne \varnothing \wedge {C}\in \mathrm{PsMet}\left({X}\right)\right)\to \left({X}×{X}\right)\mathrm{filGen}\mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)\in \mathrm{UnifOn}\left({X}\right)$
22 3 5 21 syl2anc ${⊢}{\phi }\to \left({X}×{X}\right)\mathrm{filGen}\mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)\in \mathrm{UnifOn}\left({X}\right)$
23 oveq2 ${⊢}{b}={d}\to \left[0,{b}\right)=\left[0,{d}\right)$
24 23 imaeq2d ${⊢}{b}={d}\to {{D}}^{-1}\left[\left[0,{b}\right)\right]={{D}}^{-1}\left[\left[0,{d}\right)\right]$
25 24 cbvmptv ${⊢}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)=\left({d}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{d}\right)\right]\right)$
26 25 rneqi ${⊢}\mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)=\mathrm{ran}\left({d}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{d}\right)\right]\right)$
27 26 metust ${⊢}\left({Y}\ne \varnothing \wedge {D}\in \mathrm{PsMet}\left({Y}\right)\right)\to \left({Y}×{Y}\right)\mathrm{filGen}\mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)\in \mathrm{UnifOn}\left({Y}\right)$
28 4 6 27 syl2anc ${⊢}{\phi }\to \left({Y}×{Y}\right)\mathrm{filGen}\mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)\in \mathrm{UnifOn}\left({Y}\right)$
29 oveq2 ${⊢}{a}={e}\to \left[0,{a}\right)=\left[0,{e}\right)$
30 29 imaeq2d ${⊢}{a}={e}\to {{C}}^{-1}\left[\left[0,{a}\right)\right]={{C}}^{-1}\left[\left[0,{e}\right)\right]$
31 30 cbvmptv ${⊢}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)=\left({e}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{e}\right)\right]\right)$
32 31 rneqi ${⊢}\mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)=\mathrm{ran}\left({e}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{e}\right)\right]\right)$
33 32 metustfbas ${⊢}\left({X}\ne \varnothing \wedge {C}\in \mathrm{PsMet}\left({X}\right)\right)\to \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)\in \mathrm{fBas}\left({X}×{X}\right)$
34 3 5 33 syl2anc ${⊢}{\phi }\to \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)\in \mathrm{fBas}\left({X}×{X}\right)$
35 oveq2 ${⊢}{b}={f}\to \left[0,{b}\right)=\left[0,{f}\right)$
36 35 imaeq2d ${⊢}{b}={f}\to {{D}}^{-1}\left[\left[0,{b}\right)\right]={{D}}^{-1}\left[\left[0,{f}\right)\right]$
37 36 cbvmptv ${⊢}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)=\left({f}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{f}\right)\right]\right)$
38 37 rneqi ${⊢}\mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)=\mathrm{ran}\left({f}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{f}\right)\right]\right)$
39 38 metustfbas ${⊢}\left({Y}\ne \varnothing \wedge {D}\in \mathrm{PsMet}\left({Y}\right)\right)\to \mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)\in \mathrm{fBas}\left({Y}×{Y}\right)$
40 4 6 39 syl2anc ${⊢}{\phi }\to \mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)\in \mathrm{fBas}\left({Y}×{Y}\right)$
41 15 16 22 28 34 40 isucn2 ${⊢}{\phi }\to \left({F}\in \left(\left(\left({X}×{X}\right)\mathrm{filGen}\mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)\right)\mathrm{uCn}\left(\left({Y}×{Y}\right)\mathrm{filGen}\mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)\right)\right)↔\left({F}:{X}⟶{Y}\wedge \forall {v}\in \mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{u}{y}\to {F}\left({x}\right){v}{F}\left({y}\right)\right)\right)\right)$
42 14 41 bitrd ${⊢}{\phi }\to \left({F}\in \left({U}\mathrm{uCn}{V}\right)↔\left({F}:{X}⟶{Y}\wedge \forall {v}\in \mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{u}{y}\to {F}\left({x}\right){v}{F}\left({y}\right)\right)\right)\right)$
43 eqid ${⊢}{{D}}^{-1}\left[\left[0,{d}\right)\right]={{D}}^{-1}\left[\left[0,{d}\right)\right]$
44 oveq2 ${⊢}{f}={d}\to \left[0,{f}\right)=\left[0,{d}\right)$
45 44 imaeq2d ${⊢}{f}={d}\to {{D}}^{-1}\left[\left[0,{f}\right)\right]={{D}}^{-1}\left[\left[0,{d}\right)\right]$
46 45 rspceeqv ${⊢}\left({d}\in {ℝ}^{+}\wedge {{D}}^{-1}\left[\left[0,{d}\right)\right]={{D}}^{-1}\left[\left[0,{d}\right)\right]\right)\to \exists {f}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{{D}}^{-1}\left[\left[0,{d}\right)\right]={{D}}^{-1}\left[\left[0,{f}\right)\right]$
47 43 46 mpan2 ${⊢}{d}\in {ℝ}^{+}\to \exists {f}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{{D}}^{-1}\left[\left[0,{d}\right)\right]={{D}}^{-1}\left[\left[0,{f}\right)\right]$
48 47 adantl ${⊢}\left({\phi }\wedge {d}\in {ℝ}^{+}\right)\to \exists {f}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{{D}}^{-1}\left[\left[0,{d}\right)\right]={{D}}^{-1}\left[\left[0,{f}\right)\right]$
49 38 metustel ${⊢}{D}\in \mathrm{PsMet}\left({Y}\right)\to \left({{D}}^{-1}\left[\left[0,{d}\right)\right]\in \mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)↔\exists {f}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{{D}}^{-1}\left[\left[0,{d}\right)\right]={{D}}^{-1}\left[\left[0,{f}\right)\right]\right)$
50 6 49 syl ${⊢}{\phi }\to \left({{D}}^{-1}\left[\left[0,{d}\right)\right]\in \mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)↔\exists {f}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{{D}}^{-1}\left[\left[0,{d}\right)\right]={{D}}^{-1}\left[\left[0,{f}\right)\right]\right)$
51 50 adantr ${⊢}\left({\phi }\wedge {d}\in {ℝ}^{+}\right)\to \left({{D}}^{-1}\left[\left[0,{d}\right)\right]\in \mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)↔\exists {f}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{{D}}^{-1}\left[\left[0,{d}\right)\right]={{D}}^{-1}\left[\left[0,{f}\right)\right]\right)$
52 48 51 mpbird ${⊢}\left({\phi }\wedge {d}\in {ℝ}^{+}\right)\to {{D}}^{-1}\left[\left[0,{d}\right)\right]\in \mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)$
53 26 metustel ${⊢}{D}\in \mathrm{PsMet}\left({Y}\right)\to \left({v}\in \mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)↔\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{v}={{D}}^{-1}\left[\left[0,{d}\right)\right]\right)$
54 6 53 syl ${⊢}{\phi }\to \left({v}\in \mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)↔\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{v}={{D}}^{-1}\left[\left[0,{d}\right)\right]\right)$
55 simpr ${⊢}\left({\phi }\wedge {v}={{D}}^{-1}\left[\left[0,{d}\right)\right]\right)\to {v}={{D}}^{-1}\left[\left[0,{d}\right)\right]$
56 55 breqd ${⊢}\left({\phi }\wedge {v}={{D}}^{-1}\left[\left[0,{d}\right)\right]\right)\to \left({F}\left({x}\right){v}{F}\left({y}\right)↔{F}\left({x}\right){{D}}^{-1}\left[\left[0,{d}\right)\right]{F}\left({y}\right)\right)$
57 56 imbi2d ${⊢}\left({\phi }\wedge {v}={{D}}^{-1}\left[\left[0,{d}\right)\right]\right)\to \left(\left({x}{u}{y}\to {F}\left({x}\right){v}{F}\left({y}\right)\right)↔\left({x}{u}{y}\to {F}\left({x}\right){{D}}^{-1}\left[\left[0,{d}\right)\right]{F}\left({y}\right)\right)\right)$
58 57 ralbidv ${⊢}\left({\phi }\wedge {v}={{D}}^{-1}\left[\left[0,{d}\right)\right]\right)\to \left(\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{u}{y}\to {F}\left({x}\right){v}{F}\left({y}\right)\right)↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{u}{y}\to {F}\left({x}\right){{D}}^{-1}\left[\left[0,{d}\right)\right]{F}\left({y}\right)\right)\right)$
59 58 rexralbidv ${⊢}\left({\phi }\wedge {v}={{D}}^{-1}\left[\left[0,{d}\right)\right]\right)\to \left(\exists {u}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{u}{y}\to {F}\left({x}\right){v}{F}\left({y}\right)\right)↔\exists {u}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{u}{y}\to {F}\left({x}\right){{D}}^{-1}\left[\left[0,{d}\right)\right]{F}\left({y}\right)\right)\right)$
60 52 54 59 ralxfr2d ${⊢}{\phi }\to \left(\forall {v}\in \mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{u}{y}\to {F}\left({x}\right){v}{F}\left({y}\right)\right)↔\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{u}{y}\to {F}\left({x}\right){{D}}^{-1}\left[\left[0,{d}\right)\right]{F}\left({y}\right)\right)\right)$
61 eqid ${⊢}{{C}}^{-1}\left[\left[0,{c}\right)\right]={{C}}^{-1}\left[\left[0,{c}\right)\right]$
62 oveq2 ${⊢}{e}={c}\to \left[0,{e}\right)=\left[0,{c}\right)$
63 62 imaeq2d ${⊢}{e}={c}\to {{C}}^{-1}\left[\left[0,{e}\right)\right]={{C}}^{-1}\left[\left[0,{c}\right)\right]$
64 63 rspceeqv ${⊢}\left({c}\in {ℝ}^{+}\wedge {{C}}^{-1}\left[\left[0,{c}\right)\right]={{C}}^{-1}\left[\left[0,{c}\right)\right]\right)\to \exists {e}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{{C}}^{-1}\left[\left[0,{c}\right)\right]={{C}}^{-1}\left[\left[0,{e}\right)\right]$
65 61 64 mpan2 ${⊢}{c}\in {ℝ}^{+}\to \exists {e}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{{C}}^{-1}\left[\left[0,{c}\right)\right]={{C}}^{-1}\left[\left[0,{e}\right)\right]$
66 65 adantl ${⊢}\left({\phi }\wedge {c}\in {ℝ}^{+}\right)\to \exists {e}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{{C}}^{-1}\left[\left[0,{c}\right)\right]={{C}}^{-1}\left[\left[0,{e}\right)\right]$
67 32 metustel ${⊢}{C}\in \mathrm{PsMet}\left({X}\right)\to \left({{C}}^{-1}\left[\left[0,{c}\right)\right]\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)↔\exists {e}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{{C}}^{-1}\left[\left[0,{c}\right)\right]={{C}}^{-1}\left[\left[0,{e}\right)\right]\right)$
68 5 67 syl ${⊢}{\phi }\to \left({{C}}^{-1}\left[\left[0,{c}\right)\right]\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)↔\exists {e}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{{C}}^{-1}\left[\left[0,{c}\right)\right]={{C}}^{-1}\left[\left[0,{e}\right)\right]\right)$
69 68 adantr ${⊢}\left({\phi }\wedge {c}\in {ℝ}^{+}\right)\to \left({{C}}^{-1}\left[\left[0,{c}\right)\right]\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)↔\exists {e}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{{C}}^{-1}\left[\left[0,{c}\right)\right]={{C}}^{-1}\left[\left[0,{e}\right)\right]\right)$
70 66 69 mpbird ${⊢}\left({\phi }\wedge {c}\in {ℝ}^{+}\right)\to {{C}}^{-1}\left[\left[0,{c}\right)\right]\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)$
71 20 metustel ${⊢}{C}\in \mathrm{PsMet}\left({X}\right)\to \left({u}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)↔\exists {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{u}={{C}}^{-1}\left[\left[0,{c}\right)\right]\right)$
72 5 71 syl ${⊢}{\phi }\to \left({u}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)↔\exists {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{u}={{C}}^{-1}\left[\left[0,{c}\right)\right]\right)$
73 simpr ${⊢}\left({\phi }\wedge {u}={{C}}^{-1}\left[\left[0,{c}\right)\right]\right)\to {u}={{C}}^{-1}\left[\left[0,{c}\right)\right]$
74 73 breqd ${⊢}\left({\phi }\wedge {u}={{C}}^{-1}\left[\left[0,{c}\right)\right]\right)\to \left({x}{u}{y}↔{x}{{C}}^{-1}\left[\left[0,{c}\right)\right]{y}\right)$
75 74 imbi1d ${⊢}\left({\phi }\wedge {u}={{C}}^{-1}\left[\left[0,{c}\right)\right]\right)\to \left(\left({x}{u}{y}\to {F}\left({x}\right){{D}}^{-1}\left[\left[0,{d}\right)\right]{F}\left({y}\right)\right)↔\left({x}{{C}}^{-1}\left[\left[0,{c}\right)\right]{y}\to {F}\left({x}\right){{D}}^{-1}\left[\left[0,{d}\right)\right]{F}\left({y}\right)\right)\right)$
76 75 2ralbidv ${⊢}\left({\phi }\wedge {u}={{C}}^{-1}\left[\left[0,{c}\right)\right]\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{u}{y}\to {F}\left({x}\right){{D}}^{-1}\left[\left[0,{d}\right)\right]{F}\left({y}\right)\right)↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{{C}}^{-1}\left[\left[0,{c}\right)\right]{y}\to {F}\left({x}\right){{D}}^{-1}\left[\left[0,{d}\right)\right]{F}\left({y}\right)\right)\right)$
77 70 72 76 rexxfr2d ${⊢}{\phi }\to \left(\exists {u}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{u}{y}\to {F}\left({x}\right){{D}}^{-1}\left[\left[0,{d}\right)\right]{F}\left({y}\right)\right)↔\exists {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{{C}}^{-1}\left[\left[0,{c}\right)\right]{y}\to {F}\left({x}\right){{D}}^{-1}\left[\left[0,{d}\right)\right]{F}\left({y}\right)\right)\right)$
78 77 ralbidv ${⊢}{\phi }\to \left(\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{u}{y}\to {F}\left({x}\right){{D}}^{-1}\left[\left[0,{d}\right)\right]{F}\left({y}\right)\right)↔\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{{C}}^{-1}\left[\left[0,{c}\right)\right]{y}\to {F}\left({x}\right){{D}}^{-1}\left[\left[0,{d}\right)\right]{F}\left({y}\right)\right)\right)$
79 60 78 bitrd ${⊢}{\phi }\to \left(\forall {v}\in \mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{u}{y}\to {F}\left({x}\right){v}{F}\left({y}\right)\right)↔\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{{C}}^{-1}\left[\left[0,{c}\right)\right]{y}\to {F}\left({x}\right){{D}}^{-1}\left[\left[0,{d}\right)\right]{F}\left({y}\right)\right)\right)$
80 79 adantr ${⊢}\left({\phi }\wedge {F}:{X}⟶{Y}\right)\to \left(\forall {v}\in \mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{u}{y}\to {F}\left({x}\right){v}{F}\left({y}\right)\right)↔\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{{C}}^{-1}\left[\left[0,{c}\right)\right]{y}\to {F}\left({x}\right){{D}}^{-1}\left[\left[0,{d}\right)\right]{F}\left({y}\right)\right)\right)$
81 5 ad4antr ${⊢}\left(\left(\left(\left({\phi }\wedge {F}:{X}⟶{Y}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {C}\in \mathrm{PsMet}\left({X}\right)$
82 simplr ${⊢}\left(\left(\left(\left({\phi }\wedge {F}:{X}⟶{Y}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {c}\in {ℝ}^{+}$
83 simprr ${⊢}\left(\left(\left(\left({\phi }\wedge {F}:{X}⟶{Y}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {y}\in {X}$
84 simprl ${⊢}\left(\left(\left(\left({\phi }\wedge {F}:{X}⟶{Y}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}\in {X}$
85 elbl4 ${⊢}\left(\left({C}\in \mathrm{PsMet}\left({X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({y}\in {X}\wedge {x}\in {X}\right)\right)\to \left({x}\in \left({y}\mathrm{ball}\left({C}\right){c}\right)↔{x}{{C}}^{-1}\left[\left[0,{c}\right)\right]{y}\right)$
86 rpxr ${⊢}{c}\in {ℝ}^{+}\to {c}\in {ℝ}^{*}$
87 elbl3ps ${⊢}\left(\left({C}\in \mathrm{PsMet}\left({X}\right)\wedge {c}\in {ℝ}^{*}\right)\wedge \left({y}\in {X}\wedge {x}\in {X}\right)\right)\to \left({x}\in \left({y}\mathrm{ball}\left({C}\right){c}\right)↔{x}{C}{y}<{c}\right)$
88 86 87 sylanl2 ${⊢}\left(\left({C}\in \mathrm{PsMet}\left({X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({y}\in {X}\wedge {x}\in {X}\right)\right)\to \left({x}\in \left({y}\mathrm{ball}\left({C}\right){c}\right)↔{x}{C}{y}<{c}\right)$
89 85 88 bitr3d ${⊢}\left(\left({C}\in \mathrm{PsMet}\left({X}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({y}\in {X}\wedge {x}\in {X}\right)\right)\to \left({x}{{C}}^{-1}\left[\left[0,{c}\right)\right]{y}↔{x}{C}{y}<{c}\right)$
90 81 82 83 84 89 syl22anc ${⊢}\left(\left(\left(\left({\phi }\wedge {F}:{X}⟶{Y}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left({x}{{C}}^{-1}\left[\left[0,{c}\right)\right]{y}↔{x}{C}{y}<{c}\right)$
91 6 ad4antr ${⊢}\left(\left(\left(\left({\phi }\wedge {F}:{X}⟶{Y}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {D}\in \mathrm{PsMet}\left({Y}\right)$
92 simpllr ${⊢}\left(\left(\left(\left({\phi }\wedge {F}:{X}⟶{Y}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {d}\in {ℝ}^{+}$
93 simp-4r ${⊢}\left(\left(\left(\left({\phi }\wedge {F}:{X}⟶{Y}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {F}:{X}⟶{Y}$
94 93 83 ffvelrnd ${⊢}\left(\left(\left(\left({\phi }\wedge {F}:{X}⟶{Y}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {F}\left({y}\right)\in {Y}$
95 93 84 ffvelrnd ${⊢}\left(\left(\left(\left({\phi }\wedge {F}:{X}⟶{Y}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {F}\left({x}\right)\in {Y}$
96 elbl4 ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({Y}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge \left({F}\left({y}\right)\in {Y}\wedge {F}\left({x}\right)\in {Y}\right)\right)\to \left({F}\left({x}\right)\in \left({F}\left({y}\right)\mathrm{ball}\left({D}\right){d}\right)↔{F}\left({x}\right){{D}}^{-1}\left[\left[0,{d}\right)\right]{F}\left({y}\right)\right)$
97 rpxr ${⊢}{d}\in {ℝ}^{+}\to {d}\in {ℝ}^{*}$
98 elbl3ps ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({Y}\right)\wedge {d}\in {ℝ}^{*}\right)\wedge \left({F}\left({y}\right)\in {Y}\wedge {F}\left({x}\right)\in {Y}\right)\right)\to \left({F}\left({x}\right)\in \left({F}\left({y}\right)\mathrm{ball}\left({D}\right){d}\right)↔{F}\left({x}\right){D}{F}\left({y}\right)<{d}\right)$
99 97 98 sylanl2 ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({Y}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge \left({F}\left({y}\right)\in {Y}\wedge {F}\left({x}\right)\in {Y}\right)\right)\to \left({F}\left({x}\right)\in \left({F}\left({y}\right)\mathrm{ball}\left({D}\right){d}\right)↔{F}\left({x}\right){D}{F}\left({y}\right)<{d}\right)$
100 96 99 bitr3d ${⊢}\left(\left({D}\in \mathrm{PsMet}\left({Y}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge \left({F}\left({y}\right)\in {Y}\wedge {F}\left({x}\right)\in {Y}\right)\right)\to \left({F}\left({x}\right){{D}}^{-1}\left[\left[0,{d}\right)\right]{F}\left({y}\right)↔{F}\left({x}\right){D}{F}\left({y}\right)<{d}\right)$
101 91 92 94 95 100 syl22anc ${⊢}\left(\left(\left(\left({\phi }\wedge {F}:{X}⟶{Y}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left({F}\left({x}\right){{D}}^{-1}\left[\left[0,{d}\right)\right]{F}\left({y}\right)↔{F}\left({x}\right){D}{F}\left({y}\right)<{d}\right)$
102 90 101 imbi12d ${⊢}\left(\left(\left(\left({\phi }\wedge {F}:{X}⟶{Y}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {c}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left(\left({x}{{C}}^{-1}\left[\left[0,{c}\right)\right]{y}\to {F}\left({x}\right){{D}}^{-1}\left[\left[0,{d}\right)\right]{F}\left({y}\right)\right)↔\left({x}{C}{y}<{c}\to {F}\left({x}\right){D}{F}\left({y}\right)<{d}\right)\right)$
103 102 2ralbidva ${⊢}\left(\left(\left({\phi }\wedge {F}:{X}⟶{Y}\right)\wedge {d}\in {ℝ}^{+}\right)\wedge {c}\in {ℝ}^{+}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{{C}}^{-1}\left[\left[0,{c}\right)\right]{y}\to {F}\left({x}\right){{D}}^{-1}\left[\left[0,{d}\right)\right]{F}\left({y}\right)\right)↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{C}{y}<{c}\to {F}\left({x}\right){D}{F}\left({y}\right)<{d}\right)\right)$
104 103 rexbidva ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶{Y}\right)\wedge {d}\in {ℝ}^{+}\right)\to \left(\exists {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{{C}}^{-1}\left[\left[0,{c}\right)\right]{y}\to {F}\left({x}\right){{D}}^{-1}\left[\left[0,{d}\right)\right]{F}\left({y}\right)\right)↔\exists {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{C}{y}<{c}\to {F}\left({x}\right){D}{F}\left({y}\right)<{d}\right)\right)$
105 104 ralbidva ${⊢}\left({\phi }\wedge {F}:{X}⟶{Y}\right)\to \left(\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{{C}}^{-1}\left[\left[0,{c}\right)\right]{y}\to {F}\left({x}\right){{D}}^{-1}\left[\left[0,{d}\right)\right]{F}\left({y}\right)\right)↔\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{C}{y}<{c}\to {F}\left({x}\right){D}{F}\left({y}\right)<{d}\right)\right)$
106 80 105 bitrd ${⊢}\left({\phi }\wedge {F}:{X}⟶{Y}\right)\to \left(\forall {v}\in \mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{u}{y}\to {F}\left({x}\right){v}{F}\left({y}\right)\right)↔\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{C}{y}<{c}\to {F}\left({x}\right){D}{F}\left({y}\right)<{d}\right)\right)$
107 106 pm5.32da ${⊢}{\phi }\to \left(\left({F}:{X}⟶{Y}\wedge \forall {v}\in \mathrm{ran}\left({b}\in {ℝ}^{+}⟼{{D}}^{-1}\left[\left[0,{b}\right)\right]\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({a}\in {ℝ}^{+}⟼{{C}}^{-1}\left[\left[0,{a}\right)\right]\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{u}{y}\to {F}\left({x}\right){v}{F}\left({y}\right)\right)\right)↔\left({F}:{X}⟶{Y}\wedge \forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{C}{y}<{c}\to {F}\left({x}\right){D}{F}\left({y}\right)<{d}\right)\right)\right)$
108 42 107 bitrd ${⊢}{\phi }\to \left({F}\in \left({U}\mathrm{uCn}{V}\right)↔\left({F}:{X}⟶{Y}\wedge \forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{C}{y}<{c}\to {F}\left({x}\right){D}{F}\left({y}\right)<{d}\right)\right)\right)$