Metamath Proof Explorer


Theorem limsuplt

Description: The defining property of the superior limit. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 12-Sep-2020)

Ref Expression
Hypothesis limsupval.1 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
Assertion limsuplt ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ*𝐴 ∈ ℝ* ) → ( ( lim sup ‘ 𝐹 ) < 𝐴 ↔ ∃ 𝑗 ∈ ℝ ( 𝐺𝑗 ) < 𝐴 ) )

Proof

Step Hyp Ref Expression
1 limsupval.1 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
2 1 limsuple ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ*𝐴 ∈ ℝ* ) → ( 𝐴 ≤ ( lim sup ‘ 𝐹 ) ↔ ∀ 𝑗 ∈ ℝ 𝐴 ≤ ( 𝐺𝑗 ) ) )
3 2 notbid ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ*𝐴 ∈ ℝ* ) → ( ¬ 𝐴 ≤ ( lim sup ‘ 𝐹 ) ↔ ¬ ∀ 𝑗 ∈ ℝ 𝐴 ≤ ( 𝐺𝑗 ) ) )
4 rexnal ( ∃ 𝑗 ∈ ℝ ¬ 𝐴 ≤ ( 𝐺𝑗 ) ↔ ¬ ∀ 𝑗 ∈ ℝ 𝐴 ≤ ( 𝐺𝑗 ) )
5 3 4 bitr4di ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ*𝐴 ∈ ℝ* ) → ( ¬ 𝐴 ≤ ( lim sup ‘ 𝐹 ) ↔ ∃ 𝑗 ∈ ℝ ¬ 𝐴 ≤ ( 𝐺𝑗 ) ) )
6 simp2 ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ*𝐴 ∈ ℝ* ) → 𝐹 : 𝐵 ⟶ ℝ* )
7 reex ℝ ∈ V
8 7 ssex ( 𝐵 ⊆ ℝ → 𝐵 ∈ V )
9 8 3ad2ant1 ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ*𝐴 ∈ ℝ* ) → 𝐵 ∈ V )
10 xrex * ∈ V
11 10 a1i ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ*𝐴 ∈ ℝ* ) → ℝ* ∈ V )
12 fex2 ( ( 𝐹 : 𝐵 ⟶ ℝ*𝐵 ∈ V ∧ ℝ* ∈ V ) → 𝐹 ∈ V )
13 6 9 11 12 syl3anc ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ*𝐴 ∈ ℝ* ) → 𝐹 ∈ V )
14 limsupcl ( 𝐹 ∈ V → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
15 13 14 syl ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ*𝐴 ∈ ℝ* ) → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
16 simp3 ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ*𝐴 ∈ ℝ* ) → 𝐴 ∈ ℝ* )
17 xrltnle ( ( ( lim sup ‘ 𝐹 ) ∈ ℝ*𝐴 ∈ ℝ* ) → ( ( lim sup ‘ 𝐹 ) < 𝐴 ↔ ¬ 𝐴 ≤ ( lim sup ‘ 𝐹 ) ) )
18 15 16 17 syl2anc ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ*𝐴 ∈ ℝ* ) → ( ( lim sup ‘ 𝐹 ) < 𝐴 ↔ ¬ 𝐴 ≤ ( lim sup ‘ 𝐹 ) ) )
19 1 limsupgf 𝐺 : ℝ ⟶ ℝ*
20 19 ffvelrni ( 𝑗 ∈ ℝ → ( 𝐺𝑗 ) ∈ ℝ* )
21 xrltnle ( ( ( 𝐺𝑗 ) ∈ ℝ*𝐴 ∈ ℝ* ) → ( ( 𝐺𝑗 ) < 𝐴 ↔ ¬ 𝐴 ≤ ( 𝐺𝑗 ) ) )
22 20 16 21 syl2anr ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ*𝐴 ∈ ℝ* ) ∧ 𝑗 ∈ ℝ ) → ( ( 𝐺𝑗 ) < 𝐴 ↔ ¬ 𝐴 ≤ ( 𝐺𝑗 ) ) )
23 22 rexbidva ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ*𝐴 ∈ ℝ* ) → ( ∃ 𝑗 ∈ ℝ ( 𝐺𝑗 ) < 𝐴 ↔ ∃ 𝑗 ∈ ℝ ¬ 𝐴 ≤ ( 𝐺𝑗 ) ) )
24 5 18 23 3bitr4d ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ*𝐴 ∈ ℝ* ) → ( ( lim sup ‘ 𝐹 ) < 𝐴 ↔ ∃ 𝑗 ∈ ℝ ( 𝐺𝑗 ) < 𝐴 ) )