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 ‘ 𝐹 ) < 𝐴 ↔ ∃ 𝑗 ∈ ℝ ( 𝐺 ‘ 𝑗 ) < 𝐴 ) )