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 = J
bndth.2 K = topGen ran .
bndth.3 φ J Comp
bndth.4 φ F J Cn K
evth.5 φ X
Assertion evth2 φ x X y X F x F y

Proof

Step Hyp Ref Expression
1 bndth.1 X = J
2 bndth.2 K = topGen ran .
3 bndth.3 φ J Comp
4 bndth.4 φ F J Cn K
5 evth.5 φ X
6 cmptop J Comp J Top
7 3 6 syl φ J Top
8 1 toptopon J Top J TopOn X
9 7 8 sylib φ J TopOn X
10 uniretop = topGen ran .
11 2 unieqi K = topGen ran .
12 10 11 eqtr4i = K
13 1 12 cnf F J Cn K F : X
14 4 13 syl φ F : X
15 14 feqmptd φ F = z X F z
16 15 4 eqeltrrd φ z X F z J Cn K
17 retopon topGen ran . TopOn
18 2 17 eqeltri K TopOn
19 18 a1i φ K 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 φ y 0 K Cn TopOpen fld
25 20 tgioo2 topGen ran . = TopOpen fld 𝑡
26 2 25 eqtri K = TopOpen fld 𝑡
27 ax-resscn
28 27 a1i φ
29 22 cnmptid φ y y TopOpen fld Cn TopOpen fld
30 26 22 28 29 cnmpt1res φ y y K 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 φ y 0 y K Cn TopOpen fld
34 df-neg y = 0 y
35 renegcl y y
36 34 35 eqeltrrid y 0 y
37 36 adantl φ y 0 y
38 37 fmpttd φ y 0 y :
39 38 frnd φ ran y 0 y
40 cnrest2 TopOpen fld TopOn ran y 0 y y 0 y K Cn TopOpen fld y 0 y K Cn TopOpen fld 𝑡
41 22 39 28 40 syl3anc φ y 0 y K Cn TopOpen fld y 0 y K Cn TopOpen fld 𝑡
42 33 41 mpbid φ y 0 y K Cn TopOpen fld 𝑡
43 26 oveq2i K Cn K = K Cn TopOpen fld 𝑡
44 42 43 eleqtrrdi φ y 0 y K Cn K
45 negeq y = F z y = F z
46 34 45 eqtr3id y = F z 0 y = F z
47 9 16 19 44 46 cnmpt11 φ z X F z J Cn K
48 1 2 3 47 5 evth φ x X y X z X F z y z X F z x
49 fveq2 z = y F z = F y
50 49 negeqd z = y F z = F y
51 eqid z X F z = z X F z
52 negex F y V
53 50 51 52 fvmpt y X z X F z y = F y
54 53 adantl φ x X y X z X F z y = F y
55 fveq2 z = x F z = F x
56 55 negeqd z = x F z = F x
57 negex F x V
58 56 51 57 fvmpt x X z X F z x = F x
59 58 ad2antlr φ x X y X z X F z x = F x
60 54 59 breq12d φ x X y X z X F z y z X F z x F y F x
61 14 ffvelrnda φ x X F x
62 61 adantr φ x X y X F x
63 14 ffvelrnda φ y X F y
64 63 adantlr φ x X y X F y
65 62 64 lenegd φ x X y X F x F y F y F x
66 60 65 bitr4d φ x X y X z X F z y z X F z x F x F y
67 66 ralbidva φ x X y X z X F z y z X F z x y X F x F y
68 67 rexbidva φ x X y X z X F z y z X F z x x X y X F x F y
69 48 68 mpbid φ x X y X F x F y