This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem liminflelimsuplem

Description: The superior limit is greater than or equal to the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses liminflelimsuplem.1 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
liminflelimsuplem.2 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ ( 𝑘 [,) +∞ ) ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ )
Assertion liminflelimsuplem ( 𝜑 → ( lim inf ‘ 𝐹 ) ≤ ( lim sup ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 liminflelimsuplem.1 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2 liminflelimsuplem.2 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ ( 𝑘 [,) +∞ ) ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ )
3 inss2 ⊢ ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ*
4 infxrcl ⊢ ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ* → inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ* )
5 3 4 ax-mp ⊢ inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ*
6 5 a1i ⊢ ( ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) ∧ ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) → inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ* )
7 inss2 ⊢ ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ*
8 infxrcl ⊢ ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ* → inf ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ* )
9 7 8 ax-mp ⊢ inf ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ*
10 9 a1i ⊢ ( ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) ∧ ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) → inf ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ* )
11 inss2 ⊢ ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ*
12 11 supxrcli ⊢ sup ( ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ*
13 12 a1i ⊢ ( ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) ∧ ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) → sup ( ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ* )
14 rexr ⊢ ( 𝑖 ∈ ℝ → 𝑖 ∈ ℝ* )
15 14 ad2antrr ⊢ ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) → 𝑖 ∈ ℝ* )
16 pnfxr ⊢ +∞ ∈ ℝ*
17 16 a1i ⊢ ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) → +∞ ∈ ℝ* )
18 simpr ⊢ ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) → 𝑙 ∈ ℝ )
19 simpl ⊢ ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) → 𝑖 ∈ ℝ )
20 18 19 ifcld ⊢ ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) → if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) ∈ ℝ )
21 20 rexrd ⊢ ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) → if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) ∈ ℝ* )
22 21 adantr ⊢ ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) → if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) ∈ ℝ* )
23 icossxr ⊢ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ⊆ ℝ*
24 23 sseli ⊢ ( 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) → 𝑗 ∈ ℝ* )
25 24 adantl ⊢ ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) → 𝑗 ∈ ℝ* )
26 max1 ⊢ ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) → 𝑖 ≤ if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) )
27 26 adantr ⊢ ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) → 𝑖 ≤ if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) )
28 simpr ⊢ ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) → 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) )
29 22 17 28 icogelbd ⊢ ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) → if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) ≤ 𝑗 )
30 15 22 25 27 29 xrletrd ⊢ ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) → 𝑖 ≤ 𝑗 )
31 15 17 30 icossico2d ⊢ ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) → ( 𝑗 [,) +∞ ) ⊆ ( 𝑖 [,) +∞ ) )
32 31 imass2d ⊢ ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) → ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ⊆ ( 𝐹 “ ( 𝑖 [,) +∞ ) ) )
33 32 ssrind ⊢ ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) → ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ⊆ ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) )
34 infxrss ⊢ ( ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ⊆ ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) ∧ ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ* ) → inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ inf ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
35 33 3 34 sylancl ⊢ ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) → inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ inf ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
36 35 adantr ⊢ ( ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) ∧ ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) → inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ inf ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
37 7 supxrcli ⊢ sup ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ*
38 37 a1i ⊢ ( ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) ∧ ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) → sup ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ* )
39 7 a1i ⊢ ( ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) ∧ ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) → ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ* )
40 simpr ⊢ ( ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) ∧ ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) → ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ )
41 39 40 infxrlesupxr ⊢ ( ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) ∧ ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) → inf ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
42 rexr ⊢ ( 𝑙 ∈ ℝ → 𝑙 ∈ ℝ* )
43 42 ad2antlr ⊢ ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) → 𝑙 ∈ ℝ* )
44 max2 ⊢ ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) → 𝑙 ≤ if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) )
45 44 adantr ⊢ ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) → 𝑙 ≤ if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) )
46 43 22 25 45 29 xrletrd ⊢ ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) → 𝑙 ≤ 𝑗 )
47 43 17 46 icossico2d ⊢ ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) → ( 𝑗 [,) +∞ ) ⊆ ( 𝑙 [,) +∞ ) )
48 47 imass2d ⊢ ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) → ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ⊆ ( 𝐹 “ ( 𝑙 [,) +∞ ) ) )
49 48 ssrind ⊢ ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) → ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ⊆ ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) )
50 11 a1i ⊢ ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) → ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ* )
51 49 50 xrsupssd ⊢ ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) → sup ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
52 51 adantr ⊢ ( ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) ∧ ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) → sup ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
53 10 38 13 41 52 xrletrd ⊢ ( ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) ∧ ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) → inf ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
54 6 10 13 36 53 xrletrd ⊢ ( ( ( ( 𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) ∧ ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) → inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
55 54 ad5ant2345 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ 𝑙 ∈ ℝ ) ∧ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ) ∧ ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) → inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
56 oveq1 ⊢ ( 𝑘 = if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) → ( 𝑘 [,) +∞ ) = ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) )
57 56 rexeqdv ⊢ ( 𝑘 = if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) → ( ∃ 𝑗 ∈ ( 𝑘 [,) +∞ ) ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ↔ ∃ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) )
58 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ 𝑙 ∈ ℝ ) → ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ ( 𝑘 [,) +∞ ) ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ )
59 20 adantll ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ 𝑙 ∈ ℝ ) → if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) ∈ ℝ )
60 57 58 59 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ 𝑙 ∈ ℝ ) → ∃ 𝑗 ∈ ( if ( 𝑖 ≤ 𝑙 , 𝑙 , 𝑖 ) [,) +∞ ) ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ )
61 55 60 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ 𝑙 ∈ ℝ ) → inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
62 61 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) → ∀ 𝑙 ∈ ℝ inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
63 nfv ⊢ Ⅎ 𝑙 𝜑
64 xrltso ⊢ < Or ℝ*
65 64 supex ⊢ sup ( ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ V
66 65 a1i ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℝ ) → sup ( ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ V )
67 breq2 ⊢ ( 𝑦 = sup ( ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) → ( inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ 𝑦 ↔ inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
68 63 66 67 ralrnmpt3 ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran ( 𝑙 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ 𝑦 ↔ ∀ 𝑙 ∈ ℝ inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
69 68 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) → ( ∀ 𝑦 ∈ ran ( 𝑙 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ 𝑦 ↔ ∀ 𝑙 ∈ ℝ inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
70 62 69 mpbird ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) → ∀ 𝑦 ∈ ran ( 𝑙 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ 𝑦 )
71 oveq1 ⊢ ( 𝑙 = 𝑖 → ( 𝑙 [,) +∞ ) = ( 𝑖 [,) +∞ ) )
72 71 imaeq2d ⊢ ( 𝑙 = 𝑖 → ( 𝐹 “ ( 𝑙 [,) +∞ ) ) = ( 𝐹 “ ( 𝑖 [,) +∞ ) ) )
73 72 ineq1d ⊢ ( 𝑙 = 𝑖 → ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) = ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) )
74 73 supeq1d ⊢ ( 𝑙 = 𝑖 → sup ( ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) = sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
75 74 cbvmptv ⊢ ( 𝑙 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
76 75 rneqi ⊢ ran ( 𝑙 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ran ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
77 76 raleqi ⊢ ( ∀ 𝑦 ∈ ran ( 𝑙 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ 𝑦 ↔ ∀ 𝑦 ∈ ran ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ 𝑦 )
78 70 77 sylib ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) → ∀ 𝑦 ∈ ran ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ 𝑦 )
79 3 supxrcli ⊢ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ*
80 79 rgenw ⊢ ∀ 𝑖 ∈ ℝ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ*
81 eqid ⊢ ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
82 81 rnmptss ⊢ ( ∀ 𝑖 ∈ ℝ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ* → ran ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ⊆ ℝ* )
83 80 82 ax-mp ⊢ ran ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ⊆ ℝ*
84 83 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) → ran ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ⊆ ℝ* )
85 infxrgelb ⊢ ( ( ran ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ⊆ ℝ* ∧ inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ* ) → ( inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ inf ( ran ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) ↔ ∀ 𝑦 ∈ ran ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ 𝑦 ) )
86 84 5 85 sylancl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) → ( inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ inf ( ran ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) ↔ ∀ 𝑦 ∈ ran ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ 𝑦 ) )
87 78 86 mpbird ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) → inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ inf ( ran ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
88 87 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ℝ inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ inf ( ran ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
89 nfv ⊢ Ⅎ 𝑖 𝜑
90 nfcv ⊢ Ⅎ 𝑖 ℝ
91 nfmpt1 ⊢ Ⅎ 𝑖 ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
92 91 nfrn ⊢ Ⅎ 𝑖 ran ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
93 nfcv ⊢ Ⅎ 𝑖 ℝ*
94 nfcv ⊢ Ⅎ 𝑖 <
95 92 93 94 nfinf ⊢ Ⅎ 𝑖 inf ( ran ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < )
96 5 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) → inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ* )
97 infxrcl ⊢ ( ran ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ⊆ ℝ* → inf ( ran ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) ∈ ℝ* )
98 83 97 ax-mp ⊢ inf ( ran ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) ∈ ℝ*
99 98 a1i ⊢ ( 𝜑 → inf ( ran ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) ∈ ℝ* )
100 89 90 95 96 99 supxrleubrnmptf ⊢ ( 𝜑 → ( sup ( ran ( 𝑖 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) ≤ inf ( ran ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) ↔ ∀ 𝑖 ∈ ℝ inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ inf ( ran ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) ) )
101 88 100 mpbird ⊢ ( 𝜑 → sup ( ran ( 𝑖 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) ≤ inf ( ran ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
102 eqid ⊢ ( 𝑖 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑖 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
103 1 102 liminfvald ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = sup ( ran ( 𝑖 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
104 1 81 limsupvald ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
105 101 103 104 3brtr4d ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ≤ ( lim sup ‘ 𝐹 ) )