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