# Metamath Proof Explorer

## Theorem evth

Description: The Extreme Value Theorem. A continuous function from a nonempty compact topological space to the reals attains its maximum at some point in the domain. (Contributed by Mario Carneiro, 12-Aug-2014)

Ref Expression
Hypotheses bndth.1 ${⊢}{X}=\bigcup {J}$
bndth.2 ${⊢}{K}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
bndth.3 ${⊢}{\phi }\to {J}\in \mathrm{Comp}$
bndth.4 ${⊢}{\phi }\to {F}\in \left({J}\mathrm{Cn}{K}\right)$
evth.5 ${⊢}{\phi }\to {X}\ne \varnothing$
Assertion evth ${⊢}{\phi }\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {F}\left({x}\right)$

### Proof

Step Hyp Ref Expression
1 bndth.1 ${⊢}{X}=\bigcup {J}$
2 bndth.2 ${⊢}{K}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
3 bndth.3 ${⊢}{\phi }\to {J}\in \mathrm{Comp}$
4 bndth.4 ${⊢}{\phi }\to {F}\in \left({J}\mathrm{Cn}{K}\right)$
5 evth.5 ${⊢}{\phi }\to {X}\ne \varnothing$
6 3 adantr ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to {J}\in \mathrm{Comp}$
7 cmptop ${⊢}{J}\in \mathrm{Comp}\to {J}\in \mathrm{Top}$
8 6 7 syl ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to {J}\in \mathrm{Top}$
9 1 toptopon ${⊢}{J}\in \mathrm{Top}↔{J}\in \mathrm{TopOn}\left({X}\right)$
10 8 9 sylib ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to {J}\in \mathrm{TopOn}\left({X}\right)$
11 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
12 11 cnfldtopon ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$
13 12 a1i ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$
14 1cnd ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to 1\in ℂ$
15 10 13 14 cnmptc ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to \left({z}\in {X}⟼1\right)\in \left({J}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
16 uniretop ${⊢}ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
17 2 unieqi ${⊢}\bigcup {K}=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
18 16 17 eqtr4i ${⊢}ℝ=\bigcup {K}$
19 1 18 cnf ${⊢}{F}\in \left({J}\mathrm{Cn}{K}\right)\to {F}:{X}⟶ℝ$
20 4 19 syl ${⊢}{\phi }\to {F}:{X}⟶ℝ$
21 20 frnd ${⊢}{\phi }\to \mathrm{ran}{F}\subseteq ℝ$
22 20 fdmd ${⊢}{\phi }\to \mathrm{dom}{F}={X}$
23 22 5 eqnetrd ${⊢}{\phi }\to \mathrm{dom}{F}\ne \varnothing$
24 dm0rn0 ${⊢}\mathrm{dom}{F}=\varnothing ↔\mathrm{ran}{F}=\varnothing$
25 24 necon3bii ${⊢}\mathrm{dom}{F}\ne \varnothing ↔\mathrm{ran}{F}\ne \varnothing$
26 23 25 sylib ${⊢}{\phi }\to \mathrm{ran}{F}\ne \varnothing$
27 1 2 3 4 bndth ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {x}$
28 20 ffnd ${⊢}{\phi }\to {F}Fn{X}$
29 breq1 ${⊢}{z}={F}\left({y}\right)\to \left({z}\le {x}↔{F}\left({y}\right)\le {x}\right)$
30 29 ralrn ${⊢}{F}Fn{X}\to \left(\forall {z}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{z}\le {x}↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {x}\right)$
31 28 30 syl ${⊢}{\phi }\to \left(\forall {z}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{z}\le {x}↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {x}\right)$
32 31 rexbidv ${⊢}{\phi }\to \left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{z}\le {x}↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {x}\right)$
33 27 32 mpbird ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{z}\le {x}$
34 21 26 33 3jca ${⊢}{\phi }\to \left(\mathrm{ran}{F}\subseteq ℝ\wedge \mathrm{ran}{F}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{z}\le {x}\right)$
35 suprcl ${⊢}\left(\mathrm{ran}{F}\subseteq ℝ\wedge \mathrm{ran}{F}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{z}\le {x}\right)\to sup\left(\mathrm{ran}{F},ℝ,<\right)\in ℝ$
36 34 35 syl ${⊢}{\phi }\to sup\left(\mathrm{ran}{F},ℝ,<\right)\in ℝ$
37 36 recnd ${⊢}{\phi }\to sup\left(\mathrm{ran}{F},ℝ,<\right)\in ℂ$
38 37 adantr ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to sup\left(\mathrm{ran}{F},ℝ,<\right)\in ℂ$
39 10 13 38 cnmptc ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to \left({z}\in {X}⟼sup\left(\mathrm{ran}{F},ℝ,<\right)\right)\in \left({J}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
40 20 feqmptd ${⊢}{\phi }\to {F}=\left({z}\in {X}⟼{F}\left({z}\right)\right)$
41 11 cnfldtop ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}$
42 cnrest2r ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}\to {J}\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\subseteq {J}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
43 41 42 ax-mp ${⊢}{J}\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\subseteq {J}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
44 11 tgioo2 ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ$
45 2 44 eqtri ${⊢}{K}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ$
46 45 oveq2i ${⊢}{J}\mathrm{Cn}{K}={J}\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)$
47 4 46 eleqtrdi ${⊢}{\phi }\to {F}\in \left({J}\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\right)$
48 43 47 sseldi ${⊢}{\phi }\to {F}\in \left({J}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
49 40 48 eqeltrrd ${⊢}{\phi }\to \left({z}\in {X}⟼{F}\left({z}\right)\right)\in \left({J}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
50 49 adantr ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to \left({z}\in {X}⟼{F}\left({z}\right)\right)\in \left({J}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
51 11 subcn ${⊢}-\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
52 51 a1i ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to -\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
53 10 39 50 52 cnmpt12f ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to \left({z}\in {X}⟼sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)\right)\in \left({J}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
54 36 ad2antrr ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {z}\in {X}\right)\to sup\left(\mathrm{ran}{F},ℝ,<\right)\in ℝ$
55 ffvelrn ${⊢}\left({F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\wedge {z}\in {X}\right)\to {F}\left({z}\right)\in \left(ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)$
56 55 adantll ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {z}\in {X}\right)\to {F}\left({z}\right)\in \left(ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)$
57 eldifsn ${⊢}{F}\left({z}\right)\in \left(ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)↔\left({F}\left({z}\right)\in ℝ\wedge {F}\left({z}\right)\ne sup\left(\mathrm{ran}{F},ℝ,<\right)\right)$
58 56 57 sylib ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {z}\in {X}\right)\to \left({F}\left({z}\right)\in ℝ\wedge {F}\left({z}\right)\ne sup\left(\mathrm{ran}{F},ℝ,<\right)\right)$
59 58 simpld ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {z}\in {X}\right)\to {F}\left({z}\right)\in ℝ$
60 54 59 resubcld ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {z}\in {X}\right)\to sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)\in ℝ$
61 60 recnd ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {z}\in {X}\right)\to sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)\in ℂ$
62 54 recnd ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {z}\in {X}\right)\to sup\left(\mathrm{ran}{F},ℝ,<\right)\in ℂ$
63 59 recnd ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {z}\in {X}\right)\to {F}\left({z}\right)\in ℂ$
64 58 simprd ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {z}\in {X}\right)\to {F}\left({z}\right)\ne sup\left(\mathrm{ran}{F},ℝ,<\right)$
65 64 necomd ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {z}\in {X}\right)\to sup\left(\mathrm{ran}{F},ℝ,<\right)\ne {F}\left({z}\right)$
66 62 63 65 subne0d ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {z}\in {X}\right)\to sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)\ne 0$
67 eldifsn ${⊢}sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)\in \left(ℂ\setminus \left\{0\right\}\right)↔\left(sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)\in ℂ\wedge sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)\ne 0\right)$
68 61 66 67 sylanbrc ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {z}\in {X}\right)\to sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)\in \left(ℂ\setminus \left\{0\right\}\right)$
69 68 fmpttd ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to \left({z}\in {X}⟼sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)\right):{X}⟶ℂ\setminus \left\{0\right\}$
70 69 frnd ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to \mathrm{ran}\left({z}\in {X}⟼sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)\right)\subseteq ℂ\setminus \left\{0\right\}$
71 difssd ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to ℂ\setminus \left\{0\right\}\subseteq ℂ$
72 cnrest2 ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge \mathrm{ran}\left({z}\in {X}⟼sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)\right)\subseteq ℂ\setminus \left\{0\right\}\wedge ℂ\setminus \left\{0\right\}\subseteq ℂ\right)\to \left(\left({z}\in {X}⟼sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)\right)\in \left({J}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)↔\left({z}\in {X}⟼sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)\right)\in \left({J}\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)\right)\right)$
73 13 70 71 72 syl3anc ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to \left(\left({z}\in {X}⟼sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)\right)\in \left({J}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)↔\left({z}\in {X}⟼sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)\right)\in \left({J}\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)\right)\right)$
74 53 73 mpbid ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to \left({z}\in {X}⟼sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)\right)\in \left({J}\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)\right)$
75 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)$
76 11 75 divcn ${⊢}÷\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
77 76 a1i ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to ÷\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
78 10 15 74 77 cnmpt12f ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to \left({z}\in {X}⟼\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}\right)\in \left({J}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
79 60 66 rereccld ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {z}\in {X}\right)\to \frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}\in ℝ$
80 79 fmpttd ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to \left({z}\in {X}⟼\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}\right):{X}⟶ℝ$
81 80 frnd ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to \mathrm{ran}\left({z}\in {X}⟼\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}\right)\subseteq ℝ$
82 ax-resscn ${⊢}ℝ\subseteq ℂ$
83 82 a1i ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to ℝ\subseteq ℂ$
84 cnrest2 ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge \mathrm{ran}\left({z}\in {X}⟼\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}\right)\subseteq ℝ\wedge ℝ\subseteq ℂ\right)\to \left(\left({z}\in {X}⟼\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}\right)\in \left({J}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)↔\left({z}\in {X}⟼\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}\right)\in \left({J}\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\right)\right)$
85 13 81 83 84 syl3anc ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to \left(\left({z}\in {X}⟼\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}\right)\in \left({J}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)↔\left({z}\in {X}⟼\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}\right)\in \left({J}\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\right)\right)$
86 78 85 mpbid ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to \left({z}\in {X}⟼\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}\right)\in \left({J}\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\right)$
87 86 46 eleqtrrdi ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to \left({z}\in {X}⟼\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}\right)\in \left({J}\mathrm{Cn}{K}\right)$
88 1 2 6 87 bndth ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\in {X}⟼\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}\right)\left({y}\right)\le {x}$
89 36 ad2antrr ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to sup\left(\mathrm{ran}{F},ℝ,<\right)\in ℝ$
90 simpr ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to {x}\in ℝ$
91 1re ${⊢}1\in ℝ$
92 ifcl ${⊢}\left({x}\in ℝ\wedge 1\in ℝ\right)\to if\left(1\le {x},{x},1\right)\in ℝ$
93 90 91 92 sylancl ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to if\left(1\le {x},{x},1\right)\in ℝ$
94 0red ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to 0\in ℝ$
95 91 a1i ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to 1\in ℝ$
96 0lt1 ${⊢}0<1$
97 96 a1i ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to 0<1$
98 max1 ${⊢}\left(1\in ℝ\wedge {x}\in ℝ\right)\to 1\le if\left(1\le {x},{x},1\right)$
99 91 90 98 sylancr ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to 1\le if\left(1\le {x},{x},1\right)$
100 94 95 93 97 99 ltletrd ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to 0
101 100 gt0ne0d ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to if\left(1\le {x},{x},1\right)\ne 0$
102 93 101 rereccld ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to \frac{1}{if\left(1\le {x},{x},1\right)}\in ℝ$
103 93 100 recgt0d ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to 0<\frac{1}{if\left(1\le {x},{x},1\right)}$
104 102 103 elrpd ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to \frac{1}{if\left(1\le {x},{x},1\right)}\in {ℝ}^{+}$
105 89 104 ltsubrpd ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)
106 89 102 resubcld ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)\in ℝ$
107 106 89 ltnled ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to \left(sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)
108 105 107 mpbid ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to ¬sup\left(\mathrm{ran}{F},ℝ,<\right)\le sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)$
109 simprl ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to {x}\in ℝ$
110 max2 ${⊢}\left(1\in ℝ\wedge {x}\in ℝ\right)\to {x}\le if\left(1\le {x},{x},1\right)$
111 91 109 110 sylancr ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to {x}\le if\left(1\le {x},{x},1\right)$
112 36 ad2antrr ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to sup\left(\mathrm{ran}{F},ℝ,<\right)\in ℝ$
113 ffvelrn ${⊢}\left({F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\wedge {y}\in {X}\right)\to {F}\left({y}\right)\in \left(ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)$
114 113 ad2ant2l ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to {F}\left({y}\right)\in \left(ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)$
115 eldifsn ${⊢}{F}\left({y}\right)\in \left(ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)↔\left({F}\left({y}\right)\in ℝ\wedge {F}\left({y}\right)\ne sup\left(\mathrm{ran}{F},ℝ,<\right)\right)$
116 114 115 sylib ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to \left({F}\left({y}\right)\in ℝ\wedge {F}\left({y}\right)\ne sup\left(\mathrm{ran}{F},ℝ,<\right)\right)$
117 116 simpld ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to {F}\left({y}\right)\in ℝ$
118 112 117 resubcld ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)\in ℝ$
119 fnfvelrn ${⊢}\left({F}Fn{X}\wedge {y}\in {X}\right)\to {F}\left({y}\right)\in \mathrm{ran}{F}$
120 28 119 sylan ${⊢}\left({\phi }\wedge {y}\in {X}\right)\to {F}\left({y}\right)\in \mathrm{ran}{F}$
121 suprub ${⊢}\left(\left(\mathrm{ran}{F}\subseteq ℝ\wedge \mathrm{ran}{F}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{z}\le {x}\right)\wedge {F}\left({y}\right)\in \mathrm{ran}{F}\right)\to {F}\left({y}\right)\le sup\left(\mathrm{ran}{F},ℝ,<\right)$
122 34 120 121 syl2an2r ${⊢}\left({\phi }\wedge {y}\in {X}\right)\to {F}\left({y}\right)\le sup\left(\mathrm{ran}{F},ℝ,<\right)$
123 122 ad2ant2rl ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to {F}\left({y}\right)\le sup\left(\mathrm{ran}{F},ℝ,<\right)$
124 116 simprd ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to {F}\left({y}\right)\ne sup\left(\mathrm{ran}{F},ℝ,<\right)$
125 124 necomd ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to sup\left(\mathrm{ran}{F},ℝ,<\right)\ne {F}\left({y}\right)$
126 117 112 123 125 leneltd ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to {F}\left({y}\right)
127 117 112 posdifd ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to \left({F}\left({y}\right)
128 126 127 mpbid ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to 0
129 128 gt0ne0d ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)\ne 0$
130 118 129 rereccld ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to \frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)}\in ℝ$
131 109 91 92 sylancl ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to if\left(1\le {x},{x},1\right)\in ℝ$
132 letr ${⊢}\left(\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)}\in ℝ\wedge {x}\in ℝ\wedge if\left(1\le {x},{x},1\right)\in ℝ\right)\to \left(\left(\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)}\le {x}\wedge {x}\le if\left(1\le {x},{x},1\right)\right)\to \frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)}\le if\left(1\le {x},{x},1\right)\right)$
133 130 109 131 132 syl3anc ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to \left(\left(\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)}\le {x}\wedge {x}\le if\left(1\le {x},{x},1\right)\right)\to \frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)}\le if\left(1\le {x},{x},1\right)\right)$
134 111 133 mpan2d ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to \left(\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)}\le {x}\to \frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)}\le if\left(1\le {x},{x},1\right)\right)$
135 fveq2 ${⊢}{z}={y}\to {F}\left({z}\right)={F}\left({y}\right)$
136 135 oveq2d ${⊢}{z}={y}\to sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)=sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)$
137 136 oveq2d ${⊢}{z}={y}\to \frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}=\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)}$
138 eqid ${⊢}\left({z}\in {X}⟼\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}\right)=\left({z}\in {X}⟼\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}\right)$
139 ovex ${⊢}\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)}\in \mathrm{V}$
140 137 138 139 fvmpt ${⊢}{y}\in {X}\to \left({z}\in {X}⟼\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}\right)\left({y}\right)=\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)}$
141 140 breq1d ${⊢}{y}\in {X}\to \left(\left({z}\in {X}⟼\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}\right)\left({y}\right)\le {x}↔\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)}\le {x}\right)$
142 141 ad2antll ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to \left(\left({z}\in {X}⟼\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}\right)\left({y}\right)\le {x}↔\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)}\le {x}\right)$
143 102 adantrr ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to \frac{1}{if\left(1\le {x},{x},1\right)}\in ℝ$
144 100 adantrr ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to 0
145 131 144 recgt0d ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to 0<\frac{1}{if\left(1\le {x},{x},1\right)}$
146 lerec ${⊢}\left(\left(\frac{1}{if\left(1\le {x},{x},1\right)}\in ℝ\wedge 0<\frac{1}{if\left(1\le {x},{x},1\right)}\right)\wedge \left(sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)\in ℝ\wedge 0
147 143 145 118 128 146 syl22anc ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to \left(\frac{1}{if\left(1\le {x},{x},1\right)}\le sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)↔\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)}\le \frac{1}{\frac{1}{if\left(1\le {x},{x},1\right)}}\right)$
148 lesub ${⊢}\left(\frac{1}{if\left(1\le {x},{x},1\right)}\in ℝ\wedge sup\left(\mathrm{ran}{F},ℝ,<\right)\in ℝ\wedge {F}\left({y}\right)\in ℝ\right)\to \left(\frac{1}{if\left(1\le {x},{x},1\right)}\le sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)↔{F}\left({y}\right)\le sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)\right)$
149 143 112 117 148 syl3anc ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to \left(\frac{1}{if\left(1\le {x},{x},1\right)}\le sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)↔{F}\left({y}\right)\le sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)\right)$
150 131 recnd ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to if\left(1\le {x},{x},1\right)\in ℂ$
151 101 adantrr ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to if\left(1\le {x},{x},1\right)\ne 0$
152 150 151 recrecd ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to \frac{1}{\frac{1}{if\left(1\le {x},{x},1\right)}}=if\left(1\le {x},{x},1\right)$
153 152 breq2d ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to \left(\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)}\le \frac{1}{\frac{1}{if\left(1\le {x},{x},1\right)}}↔\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)}\le if\left(1\le {x},{x},1\right)\right)$
154 147 149 153 3bitr3d ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to \left({F}\left({y}\right)\le sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)↔\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({y}\right)}\le if\left(1\le {x},{x},1\right)\right)$
155 134 142 154 3imtr4d ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge \left({x}\in ℝ\wedge {y}\in {X}\right)\right)\to \left(\left({z}\in {X}⟼\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}\right)\left({y}\right)\le {x}\to {F}\left({y}\right)\le sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)\right)$
156 155 anassrs ${⊢}\left(\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\wedge {y}\in {X}\right)\to \left(\left({z}\in {X}⟼\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}\right)\left({y}\right)\le {x}\to {F}\left({y}\right)\le sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)\right)$
157 156 ralimdva ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to \left(\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\in {X}⟼\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}\right)\left({y}\right)\le {x}\to \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)\right)$
158 34 ad2antrr ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to \left(\mathrm{ran}{F}\subseteq ℝ\wedge \mathrm{ran}{F}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{z}\le {x}\right)$
159 suprleub ${⊢}\left(\left(\mathrm{ran}{F}\subseteq ℝ\wedge \mathrm{ran}{F}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{z}\le {x}\right)\wedge sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)\in ℝ\right)\to \left(sup\left(\mathrm{ran}{F},ℝ,<\right)\le sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)↔\forall {z}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{z}\le sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)\right)$
160 158 106 159 syl2anc ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to \left(sup\left(\mathrm{ran}{F},ℝ,<\right)\le sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)↔\forall {z}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{z}\le sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)\right)$
161 28 ad2antrr ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to {F}Fn{X}$
162 breq1 ${⊢}{z}={F}\left({y}\right)\to \left({z}\le sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)↔{F}\left({y}\right)\le sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)\right)$
163 162 ralrn ${⊢}{F}Fn{X}\to \left(\forall {z}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{z}\le sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)\right)$
164 161 163 syl ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to \left(\forall {z}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{z}\le sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)\right)$
165 160 164 bitrd ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to \left(sup\left(\mathrm{ran}{F},ℝ,<\right)\le sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)\right)$
166 157 165 sylibrd ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to \left(\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\in {X}⟼\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}\right)\left({y}\right)\le {x}\to sup\left(\mathrm{ran}{F},ℝ,<\right)\le sup\left(\mathrm{ran}{F},ℝ,<\right)-\left(\frac{1}{if\left(1\le {x},{x},1\right)}\right)\right)$
167 108 166 mtod ${⊢}\left(\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\wedge {x}\in ℝ\right)\to ¬\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\in {X}⟼\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}\right)\left({y}\right)\le {x}$
168 167 nrexdv ${⊢}\left({\phi }\wedge {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\to ¬\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\in {X}⟼\frac{1}{sup\left(\mathrm{ran}{F},ℝ,<\right)-{F}\left({z}\right)}\right)\left({y}\right)\le {x}$
169 88 168 pm2.65da ${⊢}{\phi }\to ¬{F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}$
170 122 ralrimiva ${⊢}{\phi }\to \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le sup\left(\mathrm{ran}{F},ℝ,<\right)$
171 breq2 ${⊢}{F}\left({x}\right)=sup\left(\mathrm{ran}{F},ℝ,<\right)\to \left({F}\left({y}\right)\le {F}\left({x}\right)↔{F}\left({y}\right)\le sup\left(\mathrm{ran}{F},ℝ,<\right)\right)$
172 171 ralbidv ${⊢}{F}\left({x}\right)=sup\left(\mathrm{ran}{F},ℝ,<\right)\to \left(\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {F}\left({x}\right)↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le sup\left(\mathrm{ran}{F},ℝ,<\right)\right)$
173 170 172 syl5ibrcom ${⊢}{\phi }\to \left({F}\left({x}\right)=sup\left(\mathrm{ran}{F},ℝ,<\right)\to \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {F}\left({x}\right)\right)$
174 173 necon3bd ${⊢}{\phi }\to \left(¬\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {F}\left({x}\right)\to {F}\left({x}\right)\ne sup\left(\mathrm{ran}{F},ℝ,<\right)\right)$
175 174 adantr ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \left(¬\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {F}\left({x}\right)\to {F}\left({x}\right)\ne sup\left(\mathrm{ran}{F},ℝ,<\right)\right)$
176 20 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {F}\left({x}\right)\in ℝ$
177 eldifsn ${⊢}{F}\left({x}\right)\in \left(ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)↔\left({F}\left({x}\right)\in ℝ\wedge {F}\left({x}\right)\ne sup\left(\mathrm{ran}{F},ℝ,<\right)\right)$
178 177 baib ${⊢}{F}\left({x}\right)\in ℝ\to \left({F}\left({x}\right)\in \left(ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)↔{F}\left({x}\right)\ne sup\left(\mathrm{ran}{F},ℝ,<\right)\right)$
179 176 178 syl ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \left({F}\left({x}\right)\in \left(ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)↔{F}\left({x}\right)\ne sup\left(\mathrm{ran}{F},ℝ,<\right)\right)$
180 175 179 sylibrd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \left(¬\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {F}\left({x}\right)\to {F}\left({x}\right)\in \left(ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\right)$
181 180 ralimdva ${⊢}{\phi }\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}¬\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {F}\left({x}\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in \left(ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\right)$
182 ffnfv ${⊢}{F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}↔\left({F}Fn{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in \left(ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\right)$
183 182 baib ${⊢}{F}Fn{X}\to \left({F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in \left(ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\right)$
184 28 183 syl ${⊢}{\phi }\to \left({F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in \left(ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)\right)$
185 181 184 sylibrd ${⊢}{\phi }\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}¬\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {F}\left({x}\right)\to {F}:{X}⟶ℝ\setminus \left\{sup\left(\mathrm{ran}{F},ℝ,<\right)\right\}\right)$
186 169 185 mtod ${⊢}{\phi }\to ¬\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}¬\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {F}\left({x}\right)$
187 dfrex2 ${⊢}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {F}\left({x}\right)↔¬\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}¬\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {F}\left({x}\right)$
188 186 187 sylibr ${⊢}{\phi }\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {F}\left({x}\right)$