Metamath Proof Explorer

Theorem limsupval2

Description: The superior limit, relativized to an unbounded set. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 12-Sep-2020)

Ref Expression
Hypotheses limsupval.1 ⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
limsupval2.1 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
limsupval2.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
limsupval2.3 ⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
Assertion limsupval2 ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 limsupval.1 ⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
2 limsupval2.1 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
3 limsupval2.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
4 limsupval2.3 ⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
5 1 limsupval ⊢ ( 𝐹 ∈ 𝑉 → ( lim sup ‘ 𝐹 ) = inf ( ran 𝐺 , ℝ* , < ) )
6 2 5 syl ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran 𝐺 , ℝ* , < ) )
7 imassrn ⊢ ( 𝐺 “ 𝐴 ) ⊆ ran 𝐺
8 1 limsupgf ⊢ 𝐺 : ℝ ⟶ ℝ*
9 frn ⊢ ( 𝐺 : ℝ ⟶ ℝ* → ran 𝐺 ⊆ ℝ* )
10 8 9 ax-mp ⊢ ran 𝐺 ⊆ ℝ*
11 infxrlb ⊢ ( ( ran 𝐺 ⊆ ℝ* ∧ 𝑥 ∈ ran 𝐺 ) → inf ( ran 𝐺 , ℝ* , < ) ≤ 𝑥 )
12 11 ralrimiva ⊢ ( ran 𝐺 ⊆ ℝ* → ∀ 𝑥 ∈ ran 𝐺 inf ( ran 𝐺 , ℝ* , < ) ≤ 𝑥 )
13 10 12 mp1i ⊢ ( 𝜑 → ∀ 𝑥 ∈ ran 𝐺 inf ( ran 𝐺 , ℝ* , < ) ≤ 𝑥 )
14 ssralv ⊢ ( ( 𝐺 “ 𝐴 ) ⊆ ran 𝐺 → ( ∀ 𝑥 ∈ ran 𝐺 inf ( ran 𝐺 , ℝ* , < ) ≤ 𝑥 → ∀ 𝑥 ∈ ( 𝐺 “ 𝐴 ) inf ( ran 𝐺 , ℝ* , < ) ≤ 𝑥 ) )
15 7 13 14 mpsyl ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐺 “ 𝐴 ) inf ( ran 𝐺 , ℝ* , < ) ≤ 𝑥 )
16 7 10 sstri ⊢ ( 𝐺 “ 𝐴 ) ⊆ ℝ*
17 infxrcl ⊢ ( ran 𝐺 ⊆ ℝ* → inf ( ran 𝐺 , ℝ* , < ) ∈ ℝ* )
18 10 17 ax-mp ⊢ inf ( ran 𝐺 , ℝ* , < ) ∈ ℝ*
19 infxrgelb ⊢ ( ( ( 𝐺 “ 𝐴 ) ⊆ ℝ* ∧ inf ( ran 𝐺 , ℝ* , < ) ∈ ℝ* ) → ( inf ( ran 𝐺 , ℝ* , < ) ≤ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ↔ ∀ 𝑥 ∈ ( 𝐺 “ 𝐴 ) inf ( ran 𝐺 , ℝ* , < ) ≤ 𝑥 ) )
20 16 18 19 mp2an ⊢ ( inf ( ran 𝐺 , ℝ* , < ) ≤ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ↔ ∀ 𝑥 ∈ ( 𝐺 “ 𝐴 ) inf ( ran 𝐺 , ℝ* , < ) ≤ 𝑥 )
21 15 20 sylibr ⊢ ( 𝜑 → inf ( ran 𝐺 , ℝ* , < ) ≤ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) )
22 ressxr ⊢ ℝ ⊆ ℝ*
23 3 22 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )
24 supxrunb1 ⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑛 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑛 ≤ 𝑥 ↔ sup ( 𝐴 , ℝ* , < ) = +∞ ) )
25 23 24 syl ⊢ ( 𝜑 → ( ∀ 𝑛 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑛 ≤ 𝑥 ↔ sup ( 𝐴 , ℝ* , < ) = +∞ ) )
26 4 25 mpbird ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑛 ≤ 𝑥 )
27 infxrcl ⊢ ( ( 𝐺 “ 𝐴 ) ⊆ ℝ* → inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ∈ ℝ* )
28 16 27 mp1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ∈ ℝ* )
29 3 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
30 29 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
31 8 ffvelcdmi ⊢ ( 𝑥 ∈ ℝ → ( 𝐺 ‘ 𝑥 ) ∈ ℝ* )
32 30 31 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ* )
33 8 ffvelcdmi ⊢ ( 𝑛 ∈ ℝ → ( 𝐺 ‘ 𝑛 ) ∈ ℝ* )
34 33 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝐺 ‘ 𝑛 ) ∈ ℝ* )
35 ffn ⊢ ( 𝐺 : ℝ ⟶ ℝ* → 𝐺 Fn ℝ )
36 8 35 mp1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐺 Fn ℝ )
37 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐴 ⊆ ℝ )
38 simprl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑥 ∈ 𝐴 )
39 fnfvima ⊢ ( ( 𝐺 Fn ℝ ∧ 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐺 “ 𝐴 ) )
40 36 37 38 39 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐺 “ 𝐴 ) )
41 infxrlb ⊢ ( ( ( 𝐺 “ 𝐴 ) ⊆ ℝ* ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐺 “ 𝐴 ) ) → inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ ( 𝐺 ‘ 𝑥 ) )
42 16 40 41 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ ( 𝐺 ‘ 𝑥 ) )
43 simplr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑛 ∈ ℝ )
44 simprr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑛 ≤ 𝑥 )
45 limsupgord ⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑛 ≤ 𝑥 ) → sup ( ( ( 𝐹 “ ( 𝑥 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
46 43 30 44 45 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → sup ( ( ( 𝐹 “ ( 𝑥 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
47 1 limsupgval ⊢ ( 𝑥 ∈ ℝ → ( 𝐺 ‘ 𝑥 ) = sup ( ( ( 𝐹 “ ( 𝑥 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
48 30 47 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝐺 ‘ 𝑥 ) = sup ( ( ( 𝐹 “ ( 𝑥 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
49 1 limsupgval ⊢ ( 𝑛 ∈ ℝ → ( 𝐺 ‘ 𝑛 ) = sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
50 49 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝐺 ‘ 𝑛 ) = sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
51 46 48 50 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑛 ) )
52 28 32 34 42 51 xrletrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ ( 𝐺 ‘ 𝑛 ) )
53 52 rexlimdvaa ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) → ( ∃ 𝑥 ∈ 𝐴 𝑛 ≤ 𝑥 → inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ ( 𝐺 ‘ 𝑛 ) ) )
54 53 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑛 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑛 ≤ 𝑥 → ∀ 𝑛 ∈ ℝ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ ( 𝐺 ‘ 𝑛 ) ) )
55 26 54 mpd ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℝ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ ( 𝐺 ‘ 𝑛 ) )
56 8 35 ax-mp ⊢ 𝐺 Fn ℝ
57 breq2 ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑛 ) → ( inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ 𝑥 ↔ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ ( 𝐺 ‘ 𝑛 ) ) )
58 57 ralrn ⊢ ( 𝐺 Fn ℝ → ( ∀ 𝑥 ∈ ran 𝐺 inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ 𝑥 ↔ ∀ 𝑛 ∈ ℝ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ ( 𝐺 ‘ 𝑛 ) ) )
59 56 58 ax-mp ⊢ ( ∀ 𝑥 ∈ ran 𝐺 inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ 𝑥 ↔ ∀ 𝑛 ∈ ℝ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ ( 𝐺 ‘ 𝑛 ) )
60 55 59 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ ran 𝐺 inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ 𝑥 )
61 16 27 ax-mp ⊢ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ∈ ℝ*
62 infxrgelb ⊢ ( ( ran 𝐺 ⊆ ℝ* ∧ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ∈ ℝ* ) → ( inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ inf ( ran 𝐺 , ℝ* , < ) ↔ ∀ 𝑥 ∈ ran 𝐺 inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ 𝑥 ) )
63 10 61 62 mp2an ⊢ ( inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ inf ( ran 𝐺 , ℝ* , < ) ↔ ∀ 𝑥 ∈ ran 𝐺 inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ 𝑥 )
64 60 63 sylibr ⊢ ( 𝜑 → inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ inf ( ran 𝐺 , ℝ* , < ) )
65 xrletri3 ⊢ ( ( inf ( ran 𝐺 , ℝ* , < ) ∈ ℝ* ∧ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ∈ ℝ* ) → ( inf ( ran 𝐺 , ℝ* , < ) = inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ↔ ( inf ( ran 𝐺 , ℝ* , < ) ≤ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ∧ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ inf ( ran 𝐺 , ℝ* , < ) ) ) )
66 18 61 65 mp2an ⊢ ( inf ( ran 𝐺 , ℝ* , < ) = inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ↔ ( inf ( ran 𝐺 , ℝ* , < ) ≤ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ∧ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ inf ( ran 𝐺 , ℝ* , < ) ) )
67 21 64 66 sylanbrc ⊢ ( 𝜑 → inf ( ran 𝐺 , ℝ* , < ) = inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) )
68 6 67 eqtrd ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) )