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 ffvelrni ( 𝑥 ∈ ℝ → ( 𝐺𝑥 ) ∈ ℝ* )
32 30 31 syl ( ( ( 𝜑𝑛 ∈ ℝ ) ∧ ( 𝑥𝐴𝑛𝑥 ) ) → ( 𝐺𝑥 ) ∈ ℝ* )
33 8 ffvelrni ( 𝑛 ∈ ℝ → ( 𝐺𝑛 ) ∈ ℝ* )
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 ( ( 𝐺𝐴 ) , ℝ* , < ) )