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	⊢ 𝑋 = ∪ 𝐽
	bndth.2	⊢ 𝐾 = ( topGen ‘ ran (,) )
	bndth.3	⊢ ( 𝜑 → 𝐽 ∈ Comp )
	bndth.4	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
	evth.5	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
Assertion	evth2	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		bndth.1	⊢ 𝑋 = ∪ 𝐽
2		bndth.2	⊢ 𝐾 = ( topGen ‘ ran (,) )
3		bndth.3	⊢ ( 𝜑 → 𝐽 ∈ Comp )
4		bndth.4	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
5		evth.5	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
6		cmptop	⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ Top )
7	3 6	syl	⊢ ( 𝜑 → 𝐽 ∈ Top )
8	1	toptopon	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
9	7 8	sylib	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
10		uniretop	⊢ ℝ = ∪ ( topGen ‘ ran (,) )
11	2	unieqi	⊢ ∪ 𝐾 = ∪ ( topGen ‘ ran (,) )
12	10 11	eqtr4i	⊢ ℝ = ∪ 𝐾
13	1 12	cnf	⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : 𝑋 ⟶ ℝ )
14	4 13	syl	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ )
15	14	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑧 ) ) )
16	15 4	eqeltrrd	⊢ ( 𝜑 → ( 𝑧 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑧 ) ) ∈ ( 𝐽 Cn 𝐾 ) )
17		retopon	⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
18	2 17	eqeltri	⊢ 𝐾 ∈ ( TopOn ‘ ℝ )
19	18	a1i	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ℝ ) )
20		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
21	20	cnfldtopon	⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
22	21	a1i	⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
23		0cnd	⊢ ( 𝜑 → 0 ∈ ℂ )
24	19 22 23	cnmptc	⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ 0 ) ∈ ( 𝐾 Cn ( TopOpen ‘ ℂfld ) ) )
25		tgioo4	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
26	2 25	eqtri	⊢ 𝐾 = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
27		ax-resscn	⊢ ℝ ⊆ ℂ
28	27	a1i	⊢ ( 𝜑 → ℝ ⊆ ℂ )
29	22	cnmptid	⊢ ( 𝜑 → ( 𝑦 ∈ ℂ ↦ 𝑦 ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
30	26 22 28 29	cnmpt1res	⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ 𝑦 ) ∈ ( 𝐾 Cn ( TopOpen ‘ ℂfld ) ) )
31	20	subcn	⊢ − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
32	31	a1i	⊢ ( 𝜑 → − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
33	19 24 30 32	cnmpt12f	⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ∈ ( 𝐾 Cn ( TopOpen ‘ ℂfld ) ) )
34		df-neg	⊢ - 𝑦 = ( 0 − 𝑦 )
35		renegcl	⊢ ( 𝑦 ∈ ℝ → - 𝑦 ∈ ℝ )
36	34 35	eqeltrrid	⊢ ( 𝑦 ∈ ℝ → ( 0 − 𝑦 ) ∈ ℝ )
37	36	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 0 − 𝑦 ) ∈ ℝ )
38	37	fmpttd	⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) : ℝ ⟶ ℝ )
39	38	frnd	⊢ ( 𝜑 → ran ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ⊆ ℝ )
40		cnrest2	⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ran ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ⊆ ℝ ∧ ℝ ⊆ ℂ ) → ( ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ∈ ( 𝐾 Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ∈ ( 𝐾 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) )
41	22 39 28 40	syl3anc	⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ∈ ( 𝐾 Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ∈ ( 𝐾 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) )
42	33 41	mpbid	⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ∈ ( 𝐾 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) )
43	26	oveq2i	⊢ ( 𝐾 Cn 𝐾 ) = ( 𝐾 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
44	42 43	eleqtrrdi	⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ∈ ( 𝐾 Cn 𝐾 ) )
45		negeq	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑧 ) → - 𝑦 = - ( 𝐹 ‘ 𝑧 ) )
46	34 45	eqtr3id	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑧 ) → ( 0 − 𝑦 ) = - ( 𝐹 ‘ 𝑧 ) )
47	9 16 19 44 46	cnmpt11	⊢ ( 𝜑 → ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ∈ ( 𝐽 Cn 𝐾 ) )
48	1 2 3 47 5	evth	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑦 ) ≤ ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) )
49		fveq2	⊢ ( 𝑧 = 𝑦 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) )
50	49	negeqd	⊢ ( 𝑧 = 𝑦 → - ( 𝐹 ‘ 𝑧 ) = - ( 𝐹 ‘ 𝑦 ) )
51		eqid	⊢ ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) = ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) )
52		negex	⊢ - ( 𝐹 ‘ 𝑦 ) ∈ V
53	50 51 52	fvmpt	⊢ ( 𝑦 ∈ 𝑋 → ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑦 ) = - ( 𝐹 ‘ 𝑦 ) )
54	53	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑦 ) = - ( 𝐹 ‘ 𝑦 ) )
55		fveq2	⊢ ( 𝑧 = 𝑥 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
56	55	negeqd	⊢ ( 𝑧 = 𝑥 → - ( 𝐹 ‘ 𝑧 ) = - ( 𝐹 ‘ 𝑥 ) )
57		negex	⊢ - ( 𝐹 ‘ 𝑥 ) ∈ V
58	56 51 57	fvmpt	⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) = - ( 𝐹 ‘ 𝑥 ) )
59	58	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) = - ( 𝐹 ‘ 𝑥 ) )
60	54 59	breq12d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑦 ) ≤ ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) ↔ - ( 𝐹 ‘ 𝑦 ) ≤ - ( 𝐹 ‘ 𝑥 ) ) )
61	14	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
62	61	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
63	14	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
64	63	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
65	62 64	lenegd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ↔ - ( 𝐹 ‘ 𝑦 ) ≤ - ( 𝐹 ‘ 𝑥 ) ) )
66	60 65	bitr4d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑦 ) ≤ ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
67	66	ralbidva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ 𝑋 ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑦 ) ≤ ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
68	67	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑦 ) ≤ ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
69	48 68	mpbid	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) )