Step |
Hyp |
Ref |
Expression |
1 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
2 |
|
elico2 |
⊢ ( ( 𝐴 ∈ ℝ ∧ +∞ ∈ ℝ* ) → ( 𝐵 ∈ ( 𝐴 [,) +∞ ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 < +∞ ) ) ) |
3 |
1 2
|
mpan2 |
⊢ ( 𝐴 ∈ ℝ → ( 𝐵 ∈ ( 𝐴 [,) +∞ ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 < +∞ ) ) ) |
4 |
|
ltpnf |
⊢ ( 𝐵 ∈ ℝ → 𝐵 < +∞ ) |
5 |
4
|
adantr |
⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐵 < +∞ ) |
6 |
5
|
pm4.71i |
⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ↔ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ 𝐵 < +∞ ) ) |
7 |
|
df-3an |
⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 < +∞ ) ↔ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ 𝐵 < +∞ ) ) |
8 |
6 7
|
bitr4i |
⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 < +∞ ) ) |
9 |
3 8
|
bitr4di |
⊢ ( 𝐴 ∈ ℝ → ( 𝐵 ∈ ( 𝐴 [,) +∞ ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ) ) |