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 𝐹 , ℝ , < ) ) )