Metamath Proof Explorer

Theorem rfcnnnub

Description: Given a real continuous function F defined on a compact topological space, there is always a positive integer that is a strict upper bound of its range. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses rfcnnnub.1 ⊢ Ⅎ 𝑡 𝐹
rfcnnnub.2 ⊢ Ⅎ 𝑡 𝜑
rfcnnnub.3 ⊢ 𝐾 = ( topGen ‘ ran (,) )
rfcnnnub.4 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
rfcnnnub.5 ⊢ 𝑇 = ∪ 𝐽
rfcnnnub.6 ⊢ ( 𝜑 → 𝑇 ≠ ∅ )
rfcnnnub.7 ⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
rfcnnnub.8 ⊢ ( 𝜑 → 𝐹 ∈ 𝐶 )
Assertion rfcnnnub ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑛 )

Proof

Step Hyp Ref Expression
1 rfcnnnub.1 ⊢ Ⅎ 𝑡 𝐹
2 rfcnnnub.2 ⊢ Ⅎ 𝑡 𝜑
3 rfcnnnub.3 ⊢ 𝐾 = ( topGen ‘ ran (,) )
4 rfcnnnub.4 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
5 rfcnnnub.5 ⊢ 𝑇 = ∪ 𝐽
6 rfcnnnub.6 ⊢ ( 𝜑 → 𝑇 ≠ ∅ )
7 rfcnnnub.7 ⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
8 rfcnnnub.8 ⊢ ( 𝜑 → 𝐹 ∈ 𝐶 )
9 nfcv ⊢ Ⅎ 𝑠 𝐹
10 nfcv ⊢ Ⅎ 𝑠 𝑇
11 nfcv ⊢ Ⅎ 𝑡 𝑇
12 nfv ⊢ Ⅎ 𝑠 𝜑
13 8 7 eleqtrdi ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
14 9 1 10 11 12 2 5 3 4 13 6 evthf ⊢ ( 𝜑 → ∃ 𝑠 ∈ 𝑇 ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) )
15 df-rex ⊢ ( ∃ 𝑠 ∈ 𝑇 ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ) )
16 14 15 sylib ⊢ ( 𝜑 → ∃ 𝑠 ( 𝑠 ∈ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ) )
17 3 5 7 8 fcnre ⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ ℝ )
18 17 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑠 ) ∈ ℝ )
19 18 ex ⊢ ( 𝜑 → ( 𝑠 ∈ 𝑇 → ( 𝐹 ‘ 𝑠 ) ∈ ℝ ) )
20 19 anim1d ⊢ ( 𝜑 → ( ( 𝑠 ∈ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ) → ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ) ) )
21 20 eximdv ⊢ ( 𝜑 → ( ∃ 𝑠 ( 𝑠 ∈ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ) → ∃ 𝑠 ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ) ) )
22 16 21 mpd ⊢ ( 𝜑 → ∃ 𝑠 ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ) )
23 17 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
24 23 ex ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 → ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) )
25 2 24 ralrimi ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
26 19.41v ⊢ ( ∃ 𝑠 ( ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) ↔ ( ∃ 𝑠 ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) )
27 22 25 26 sylanbrc ⊢ ( 𝜑 → ∃ 𝑠 ( ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) )
28 df-3an ⊢ ( ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) ↔ ( ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) )
29 28 exbii ⊢ ( ∃ 𝑠 ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) ↔ ∃ 𝑠 ( ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) )
30 27 29 sylibr ⊢ ( 𝜑 → ∃ 𝑠 ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) )
31 nfcv ⊢ Ⅎ 𝑡 𝑠
32 1 31 nffv ⊢ Ⅎ 𝑡 ( 𝐹 ‘ 𝑠 )
33 32 nfel1 ⊢ Ⅎ 𝑡 ( 𝐹 ‘ 𝑠 ) ∈ ℝ
34 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 )
35 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ
36 33 34 35 nf3an ⊢ Ⅎ 𝑡 ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
37 nfv ⊢ Ⅎ 𝑡 𝑛 ∈ ℕ
38 nfcv ⊢ Ⅎ 𝑡 <
39 nfcv ⊢ Ⅎ 𝑡 𝑛
40 32 38 39 nfbr ⊢ Ⅎ 𝑡 ( 𝐹 ‘ 𝑠 ) < 𝑛
41 37 40 nfan ⊢ Ⅎ 𝑡 ( 𝑛 ∈ ℕ ∧ ( 𝐹 ‘ 𝑠 ) < 𝑛 )
42 36 41 nfan ⊢ Ⅎ 𝑡 ( ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝐹 ‘ 𝑠 ) < 𝑛 ) )
43 simpll3 ⊢ ( ( ( ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝐹 ‘ 𝑠 ) < 𝑛 ) ) ∧ 𝑡 ∈ 𝑇 ) → ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
44 simpr ⊢ ( ( ( ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝐹 ‘ 𝑠 ) < 𝑛 ) ) ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 )
45 rsp ⊢ ( ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ → ( 𝑡 ∈ 𝑇 → ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) )
46 43 44 45 sylc ⊢ ( ( ( ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝐹 ‘ 𝑠 ) < 𝑛 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
47 simpll1 ⊢ ( ( ( ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝐹 ‘ 𝑠 ) < 𝑛 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑠 ) ∈ ℝ )
48 simplrl ⊢ ( ( ( ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝐹 ‘ 𝑠 ) < 𝑛 ) ) ∧ 𝑡 ∈ 𝑇 ) → 𝑛 ∈ ℕ )
49 48 nnred ⊢ ( ( ( ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝐹 ‘ 𝑠 ) < 𝑛 ) ) ∧ 𝑡 ∈ 𝑇 ) → 𝑛 ∈ ℝ )
50 simpl2 ⊢ ( ( ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝐹 ‘ 𝑠 ) < 𝑛 ) ) → ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) )
51 50 r19.21bi ⊢ ( ( ( ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝐹 ‘ 𝑠 ) < 𝑛 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) )
52 simplrr ⊢ ( ( ( ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝐹 ‘ 𝑠 ) < 𝑛 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑠 ) < 𝑛 )
53 46 47 49 51 52 lelttrd ⊢ ( ( ( ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝐹 ‘ 𝑠 ) < 𝑛 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) < 𝑛 )
54 53 ex ⊢ ( ( ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝐹 ‘ 𝑠 ) < 𝑛 ) ) → ( 𝑡 ∈ 𝑇 → ( 𝐹 ‘ 𝑡 ) < 𝑛 ) )
55 42 54 ralrimi ⊢ ( ( ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝐹 ‘ 𝑠 ) < 𝑛 ) ) → ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑛 )
56 arch ⊢ ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ → ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑠 ) < 𝑛 )
57 56 3ad2ant1 ⊢ ( ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) → ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑠 ) < 𝑛 )
58 55 57 reximddv ⊢ ( ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) → ∃ 𝑛 ∈ ℕ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑛 )
59 58 eximi ⊢ ( ∃ 𝑠 ( ( 𝐹 ‘ 𝑠 ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑠 ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ∈ ℝ ) → ∃ 𝑠 ∃ 𝑛 ∈ ℕ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑛 )
60 30 59 syl ⊢ ( 𝜑 → ∃ 𝑠 ∃ 𝑛 ∈ ℕ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑛 )
61 19.9v ⊢ ( ∃ 𝑠 ∃ 𝑛 ∈ ℕ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑛 ↔ ∃ 𝑛 ∈ ℕ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑛 )
62 60 61 sylib ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑛 )