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\forall y\in XF\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}\leftrightarrow 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){\upharpoonright }_{𝑡}ℝ$$
26	2 25	eqtri	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$
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){\times }_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){\times }_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)\leftrightarrow \left(y\in ℝ⟼0-y\right)\in \left(K\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\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)\leftrightarrow \left(y\in ℝ⟼0-y\right)\in \left(K\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\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){\upharpoonright }_{𝑡}ℝ\right)\right)$$
43	26	oveq2i	$$⊢K\mathrm{Cn}K=K\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\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	eqtr3id	$$⊢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\forall y\in X\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)\leftrightarrow -F\left(y\right)\le -F\left(x\right)\right)$$
61	14	ffvelcdmda	$$⊢\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	ffvelcdmda	$$⊢\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)\leftrightarrow -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)\leftrightarrow 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\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)\leftrightarrow \forall y\in XF\left(x\right)\le F\left(y\right)\right)$$
68	67	rexbidva	$$⊢\phi \to \left(\exists x\in X\forall y\in X\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)\leftrightarrow \exists x\in X\forall y\in XF\left(x\right)\le F\left(y\right)\right)$$
69	48 68	mpbid	$$⊢\phi \to \exists x\in X\forall y\in XF\left(x\right)\le F\left(y\right)$$