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