Metamath Proof Explorer


Theorem cncmpmax

Description: When the hypothesis for the extreme value theorem hold, then the sup of the range of the function belongs to the range, it is real and it an upper bound of the range. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses cncmpmax.1 𝑇 = 𝐽
cncmpmax.2 𝐾 = ( topGen ‘ ran (,) )
cncmpmax.3 ( 𝜑𝐽 ∈ Comp )
cncmpmax.4 ( 𝜑𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
cncmpmax.5 ( 𝜑𝑇 ≠ ∅ )
Assertion cncmpmax ( 𝜑 → ( sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 ∧ sup ( ran 𝐹 , ℝ , < ) ∈ ℝ ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ sup ( ran 𝐹 , ℝ , < ) ) )

Proof

Step Hyp Ref Expression
1 cncmpmax.1 𝑇 = 𝐽
2 cncmpmax.2 𝐾 = ( topGen ‘ ran (,) )
3 cncmpmax.3 ( 𝜑𝐽 ∈ Comp )
4 cncmpmax.4 ( 𝜑𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
5 cncmpmax.5 ( 𝜑𝑇 ≠ ∅ )
6 1 2 3 4 5 evth ( 𝜑 → ∃ 𝑥𝑇𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) )
7 eqid ( 𝐽 Cn 𝐾 ) = ( 𝐽 Cn 𝐾 )
8 2 1 7 4 fcnre ( 𝜑𝐹 : 𝑇 ⟶ ℝ )
9 8 frnd ( 𝜑 → ran 𝐹 ⊆ ℝ )
10 9 adantr ( ( 𝜑 ∧ ( 𝑥𝑇 ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ) ) → ran 𝐹 ⊆ ℝ )
11 8 ffund ( 𝜑 → Fun 𝐹 )
12 11 adantr ( ( 𝜑𝑥𝑇 ) → Fun 𝐹 )
13 simpr ( ( 𝜑𝑥𝑇 ) → 𝑥𝑇 )
14 8 adantr ( ( 𝜑𝑥𝑇 ) → 𝐹 : 𝑇 ⟶ ℝ )
15 14 fdmd ( ( 𝜑𝑥𝑇 ) → dom 𝐹 = 𝑇 )
16 13 15 eleqtrrd ( ( 𝜑𝑥𝑇 ) → 𝑥 ∈ dom 𝐹 )
17 fvelrn ( ( Fun 𝐹𝑥 ∈ dom 𝐹 ) → ( 𝐹𝑥 ) ∈ ran 𝐹 )
18 12 16 17 syl2anc ( ( 𝜑𝑥𝑇 ) → ( 𝐹𝑥 ) ∈ ran 𝐹 )
19 18 adantrr ( ( 𝜑 ∧ ( 𝑥𝑇 ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ) ) → ( 𝐹𝑥 ) ∈ ran 𝐹 )
20 ffn ( 𝐹 : 𝑇 ⟶ ℝ → 𝐹 Fn 𝑇 )
21 fvelrnb ( 𝐹 Fn 𝑇 → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑠𝑇 ( 𝐹𝑠 ) = 𝑦 ) )
22 8 20 21 3syl ( 𝜑 → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑠𝑇 ( 𝐹𝑠 ) = 𝑦 ) )
23 22 biimpa ( ( 𝜑𝑦 ∈ ran 𝐹 ) → ∃ 𝑠𝑇 ( 𝐹𝑠 ) = 𝑦 )
24 df-rex ( ∃ 𝑠𝑇 ( 𝐹𝑠 ) = 𝑦 ↔ ∃ 𝑠 ( 𝑠𝑇 ∧ ( 𝐹𝑠 ) = 𝑦 ) )
25 23 24 sylib ( ( 𝜑𝑦 ∈ ran 𝐹 ) → ∃ 𝑠 ( 𝑠𝑇 ∧ ( 𝐹𝑠 ) = 𝑦 ) )
26 25 adantlr ( ( ( 𝜑 ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ∃ 𝑠 ( 𝑠𝑇 ∧ ( 𝐹𝑠 ) = 𝑦 ) )
27 simprr ( ( ( ( 𝜑 ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ ( 𝑠𝑇 ∧ ( 𝐹𝑠 ) = 𝑦 ) ) → ( 𝐹𝑠 ) = 𝑦 )
28 simpllr ( ( ( ( 𝜑 ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ ( 𝑠𝑇 ∧ ( 𝐹𝑠 ) = 𝑦 ) ) → ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) )
29 simprl ( ( ( ( 𝜑 ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ ( 𝑠𝑇 ∧ ( 𝐹𝑠 ) = 𝑦 ) ) → 𝑠𝑇 )
30 fveq2 ( 𝑡 = 𝑠 → ( 𝐹𝑡 ) = ( 𝐹𝑠 ) )
31 30 breq1d ( 𝑡 = 𝑠 → ( ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ↔ ( 𝐹𝑠 ) ≤ ( 𝐹𝑥 ) ) )
32 31 rspccva ( ( ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ∧ 𝑠𝑇 ) → ( 𝐹𝑠 ) ≤ ( 𝐹𝑥 ) )
33 28 29 32 syl2anc ( ( ( ( 𝜑 ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ ( 𝑠𝑇 ∧ ( 𝐹𝑠 ) = 𝑦 ) ) → ( 𝐹𝑠 ) ≤ ( 𝐹𝑥 ) )
34 27 33 eqbrtrrd ( ( ( ( 𝜑 ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ ( 𝑠𝑇 ∧ ( 𝐹𝑠 ) = 𝑦 ) ) → 𝑦 ≤ ( 𝐹𝑥 ) )
35 26 34 exlimddv ( ( ( 𝜑 ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ≤ ( 𝐹𝑥 ) )
36 35 ralrimiva ( ( 𝜑 ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ) → ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ ( 𝐹𝑥 ) )
37 36 adantrl ( ( 𝜑 ∧ ( 𝑥𝑇 ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ) ) → ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ ( 𝐹𝑥 ) )
38 ubelsupr ( ( ran 𝐹 ⊆ ℝ ∧ ( 𝐹𝑥 ) ∈ ran 𝐹 ∧ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ ( 𝐹𝑥 ) ) → ( 𝐹𝑥 ) = sup ( ran 𝐹 , ℝ , < ) )
39 10 19 37 38 syl3anc ( ( 𝜑 ∧ ( 𝑥𝑇 ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ) ) → ( 𝐹𝑥 ) = sup ( ran 𝐹 , ℝ , < ) )
40 39 eqcomd ( ( 𝜑 ∧ ( 𝑥𝑇 ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ) ) → sup ( ran 𝐹 , ℝ , < ) = ( 𝐹𝑥 ) )
41 40 19 eqeltrd ( ( 𝜑 ∧ ( 𝑥𝑇 ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ) ) → sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 )
42 10 41 sseldd ( ( 𝜑 ∧ ( 𝑥𝑇 ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ) ) → sup ( ran 𝐹 , ℝ , < ) ∈ ℝ )
43 simplrr ( ( ( 𝜑 ∧ ( 𝑥𝑇 ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ) ) ∧ 𝑠𝑇 ) → ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) )
44 43 32 sylancom ( ( ( 𝜑 ∧ ( 𝑥𝑇 ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ) ) ∧ 𝑠𝑇 ) → ( 𝐹𝑠 ) ≤ ( 𝐹𝑥 ) )
45 40 adantr ( ( ( 𝜑 ∧ ( 𝑥𝑇 ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ) ) ∧ 𝑠𝑇 ) → sup ( ran 𝐹 , ℝ , < ) = ( 𝐹𝑥 ) )
46 44 45 breqtrrd ( ( ( 𝜑 ∧ ( 𝑥𝑇 ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ) ) ∧ 𝑠𝑇 ) → ( 𝐹𝑠 ) ≤ sup ( ran 𝐹 , ℝ , < ) )
47 46 ralrimiva ( ( 𝜑 ∧ ( 𝑥𝑇 ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ) ) → ∀ 𝑠𝑇 ( 𝐹𝑠 ) ≤ sup ( ran 𝐹 , ℝ , < ) )
48 30 breq1d ( 𝑡 = 𝑠 → ( ( 𝐹𝑡 ) ≤ sup ( ran 𝐹 , ℝ , < ) ↔ ( 𝐹𝑠 ) ≤ sup ( ran 𝐹 , ℝ , < ) ) )
49 48 cbvralvw ( ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ sup ( ran 𝐹 , ℝ , < ) ↔ ∀ 𝑠𝑇 ( 𝐹𝑠 ) ≤ sup ( ran 𝐹 , ℝ , < ) )
50 47 49 sylibr ( ( 𝜑 ∧ ( 𝑥𝑇 ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ) ) → ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ sup ( ran 𝐹 , ℝ , < ) )
51 41 42 50 3jca ( ( 𝜑 ∧ ( 𝑥𝑇 ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ ( 𝐹𝑥 ) ) ) → ( sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 ∧ sup ( ran 𝐹 , ℝ , < ) ∈ ℝ ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ sup ( ran 𝐹 , ℝ , < ) ) )
52 6 51 rexlimddv ( 𝜑 → ( sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 ∧ sup ( ran 𝐹 , ℝ , < ) ∈ ℝ ∧ ∀ 𝑡𝑇 ( 𝐹𝑡 ) ≤ sup ( ran 𝐹 , ℝ , < ) ) )