Step 
Hyp 
Ref 
Expression 
1 

mnfxr 
⊢ ∞ ∈ ℝ^{*} 
2 

pnfxr 
⊢ +∞ ∈ ℝ^{*} 
3 

iccval 
⊢ ( ( ∞ ∈ ℝ^{*} ∧ +∞ ∈ ℝ^{*} ) → ( ∞ [,] +∞ ) = { 𝑥 ∈ ℝ^{*} ∣ ( ∞ ≤ 𝑥 ∧ 𝑥 ≤ +∞ ) } ) 
4 
1 2 3

mp2an 
⊢ ( ∞ [,] +∞ ) = { 𝑥 ∈ ℝ^{*} ∣ ( ∞ ≤ 𝑥 ∧ 𝑥 ≤ +∞ ) } 
5 

rabid2 
⊢ ( ℝ^{*} = { 𝑥 ∈ ℝ^{*} ∣ ( ∞ ≤ 𝑥 ∧ 𝑥 ≤ +∞ ) } ↔ ∀ 𝑥 ∈ ℝ^{*} ( ∞ ≤ 𝑥 ∧ 𝑥 ≤ +∞ ) ) 
6 

mnfle 
⊢ ( 𝑥 ∈ ℝ^{*} → ∞ ≤ 𝑥 ) 
7 

pnfge 
⊢ ( 𝑥 ∈ ℝ^{*} → 𝑥 ≤ +∞ ) 
8 
6 7

jca 
⊢ ( 𝑥 ∈ ℝ^{*} → ( ∞ ≤ 𝑥 ∧ 𝑥 ≤ +∞ ) ) 
9 
5 8

mprgbir 
⊢ ℝ^{*} = { 𝑥 ∈ ℝ^{*} ∣ ( ∞ ≤ 𝑥 ∧ 𝑥 ≤ +∞ ) } 
10 
4 9

eqtr4i 
⊢ ( ∞ [,] +∞ ) = ℝ^{*} 