# Metamath Proof Explorer

## Theorem evth2

Description: The Extreme Value Theorem, minimum version. A continuous function from a nonempty compact topological space to the reals attains its minimum 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 evth2 ${⊢}{\phi }\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\le {F}\left({y}\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 cmptop ${⊢}{J}\in \mathrm{Comp}\to {J}\in \mathrm{Top}$
7 3 6 syl ${⊢}{\phi }\to {J}\in \mathrm{Top}$
8 1 toptopon ${⊢}{J}\in \mathrm{Top}↔{J}\in \mathrm{TopOn}\left({X}\right)$
9 7 8 sylib ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
10 uniretop ${⊢}ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
11 2 unieqi ${⊢}\bigcup {K}=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
12 10 11 eqtr4i ${⊢}ℝ=\bigcup {K}$
13 1 12 cnf ${⊢}{F}\in \left({J}\mathrm{Cn}{K}\right)\to {F}:{X}⟶ℝ$
14 4 13 syl ${⊢}{\phi }\to {F}:{X}⟶ℝ$
15 14 feqmptd ${⊢}{\phi }\to {F}=\left({z}\in {X}⟼{F}\left({z}\right)\right)$
16 15 4 eqeltrrd ${⊢}{\phi }\to \left({z}\in {X}⟼{F}\left({z}\right)\right)\in \left({J}\mathrm{Cn}{K}\right)$
17 retopon ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{TopOn}\left(ℝ\right)$
18 2 17 eqeltri ${⊢}{K}\in \mathrm{TopOn}\left(ℝ\right)$
19 18 a1i ${⊢}{\phi }\to {K}\in \mathrm{TopOn}\left(ℝ\right)$
20 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
21 20 cnfldtopon ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$
22 21 a1i ${⊢}{\phi }\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$
23 0cnd ${⊢}{\phi }\to 0\in ℂ$
24 19 22 23 cnmptc ${⊢}{\phi }\to \left({y}\in ℝ⟼0\right)\in \left({K}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
25 20 tgioo2 ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ$
26 2 25 eqtri ${⊢}{K}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ$
27 ax-resscn ${⊢}ℝ\subseteq ℂ$
28 27 a1i ${⊢}{\phi }\to ℝ\subseteq ℂ$
29 22 cnmptid ${⊢}{\phi }\to \left({y}\in ℂ⟼{y}\right)\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
30 26 22 28 29 cnmpt1res ${⊢}{\phi }\to \left({y}\in ℝ⟼{y}\right)\in \left({K}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
31 20 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)$
32 31 a1i ${⊢}{\phi }\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)$
33 19 24 30 32 cnmpt12f ${⊢}{\phi }\to \left({y}\in ℝ⟼0-{y}\right)\in \left({K}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
34 df-neg ${⊢}-{y}=0-{y}$
35 renegcl ${⊢}{y}\in ℝ\to -{y}\in ℝ$
36 34 35 eqeltrrid ${⊢}{y}\in ℝ\to 0-{y}\in ℝ$
37 36 adantl ${⊢}\left({\phi }\wedge {y}\in ℝ\right)\to 0-{y}\in ℝ$
38 37 fmpttd ${⊢}{\phi }\to \left({y}\in ℝ⟼0-{y}\right):ℝ⟶ℝ$
39 38 frnd ${⊢}{\phi }\to \mathrm{ran}\left({y}\in ℝ⟼0-{y}\right)\subseteq ℝ$
40 cnrest2 ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge \mathrm{ran}\left({y}\in ℝ⟼0-{y}\right)\subseteq ℝ\wedge ℝ\subseteq ℂ\right)\to \left(\left({y}\in ℝ⟼0-{y}\right)\in \left({K}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)↔\left({y}\in ℝ⟼0-{y}\right)\in \left({K}\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\right)\right)$
41 22 39 28 40 syl3anc ${⊢}{\phi }\to \left(\left({y}\in ℝ⟼0-{y}\right)\in \left({K}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)↔\left({y}\in ℝ⟼0-{y}\right)\in \left({K}\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\right)\right)$
42 33 41 mpbid ${⊢}{\phi }\to \left({y}\in ℝ⟼0-{y}\right)\in \left({K}\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\right)$
43 26 oveq2i ${⊢}{K}\mathrm{Cn}{K}={K}\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)$
44 42 43 eleqtrrdi ${⊢}{\phi }\to \left({y}\in ℝ⟼0-{y}\right)\in \left({K}\mathrm{Cn}{K}\right)$
45 negeq ${⊢}{y}={F}\left({z}\right)\to -{y}=-{F}\left({z}\right)$
46 34 45 syl5eqr ${⊢}{y}={F}\left({z}\right)\to 0-{y}=-{F}\left({z}\right)$
47 9 16 19 44 46 cnmpt11 ${⊢}{\phi }\to \left({z}\in {X}⟼-{F}\left({z}\right)\right)\in \left({J}\mathrm{Cn}{K}\right)$
48 1 2 3 47 5 evth ${⊢}{\phi }\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\in {X}⟼-{F}\left({z}\right)\right)\left({y}\right)\le \left({z}\in {X}⟼-{F}\left({z}\right)\right)\left({x}\right)$
49 fveq2 ${⊢}{z}={y}\to {F}\left({z}\right)={F}\left({y}\right)$
50 49 negeqd ${⊢}{z}={y}\to -{F}\left({z}\right)=-{F}\left({y}\right)$
51 eqid ${⊢}\left({z}\in {X}⟼-{F}\left({z}\right)\right)=\left({z}\in {X}⟼-{F}\left({z}\right)\right)$
52 negex ${⊢}-{F}\left({y}\right)\in \mathrm{V}$
53 50 51 52 fvmpt ${⊢}{y}\in {X}\to \left({z}\in {X}⟼-{F}\left({z}\right)\right)\left({y}\right)=-{F}\left({y}\right)$
54 53 adantl ${⊢}\left(\left({\phi }\wedge {x}\in {X}\right)\wedge {y}\in {X}\right)\to \left({z}\in {X}⟼-{F}\left({z}\right)\right)\left({y}\right)=-{F}\left({y}\right)$
55 fveq2 ${⊢}{z}={x}\to {F}\left({z}\right)={F}\left({x}\right)$
56 55 negeqd ${⊢}{z}={x}\to -{F}\left({z}\right)=-{F}\left({x}\right)$
57 negex ${⊢}-{F}\left({x}\right)\in \mathrm{V}$
58 56 51 57 fvmpt ${⊢}{x}\in {X}\to \left({z}\in {X}⟼-{F}\left({z}\right)\right)\left({x}\right)=-{F}\left({x}\right)$
59 58 ad2antlr ${⊢}\left(\left({\phi }\wedge {x}\in {X}\right)\wedge {y}\in {X}\right)\to \left({z}\in {X}⟼-{F}\left({z}\right)\right)\left({x}\right)=-{F}\left({x}\right)$
60 54 59 breq12d ${⊢}\left(\left({\phi }\wedge {x}\in {X}\right)\wedge {y}\in {X}\right)\to \left(\left({z}\in {X}⟼-{F}\left({z}\right)\right)\left({y}\right)\le \left({z}\in {X}⟼-{F}\left({z}\right)\right)\left({x}\right)↔-{F}\left({y}\right)\le -{F}\left({x}\right)\right)$
61 14 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {F}\left({x}\right)\in ℝ$
62 61 adantr ${⊢}\left(\left({\phi }\wedge {x}\in {X}\right)\wedge {y}\in {X}\right)\to {F}\left({x}\right)\in ℝ$
63 14 ffvelrnda ${⊢}\left({\phi }\wedge {y}\in {X}\right)\to {F}\left({y}\right)\in ℝ$
64 63 adantlr ${⊢}\left(\left({\phi }\wedge {x}\in {X}\right)\wedge {y}\in {X}\right)\to {F}\left({y}\right)\in ℝ$
65 62 64 lenegd ${⊢}\left(\left({\phi }\wedge {x}\in {X}\right)\wedge {y}\in {X}\right)\to \left({F}\left({x}\right)\le {F}\left({y}\right)↔-{F}\left({y}\right)\le -{F}\left({x}\right)\right)$
66 60 65 bitr4d ${⊢}\left(\left({\phi }\wedge {x}\in {X}\right)\wedge {y}\in {X}\right)\to \left(\left({z}\in {X}⟼-{F}\left({z}\right)\right)\left({y}\right)\le \left({z}\in {X}⟼-{F}\left({z}\right)\right)\left({x}\right)↔{F}\left({x}\right)\le {F}\left({y}\right)\right)$
67 66 ralbidva ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \left(\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\in {X}⟼-{F}\left({z}\right)\right)\left({y}\right)\le \left({z}\in {X}⟼-{F}\left({z}\right)\right)\left({x}\right)↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\le {F}\left({y}\right)\right)$
68 67 rexbidva ${⊢}{\phi }\to \left(\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}\in {X}⟼-{F}\left({z}\right)\right)\left({y}\right)\le \left({z}\in {X}⟼-{F}\left({z}\right)\right)\left({x}\right)↔\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\le {F}\left({y}\right)\right)$
69 48 68 mpbid ${⊢}{\phi }\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\le {F}\left({y}\right)$