Theorem ioomax

Description: The open interval from minus to plus infinity. (Contributed by NM, 6-Feb-2007)

	Ref	Expression
Assertion	ioomax	⊢ ( -∞ (,) +∞ ) = ℝ

Proof

Step	Hyp	Ref	Expression
1		mnfxr	⊢ -∞ ∈ ℝ*
2		pnfxr	⊢ +∞ ∈ ℝ*
3		iooval2	⊢ ( ( -∞ ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( -∞ (,) +∞ ) = { 𝑥 ∈ ℝ ∣ ( -∞ < 𝑥 ∧ 𝑥 < +∞ ) } )
4	1 2 3	mp2an	⊢ ( -∞ (,) +∞ ) = { 𝑥 ∈ ℝ ∣ ( -∞ < 𝑥 ∧ 𝑥 < +∞ ) }
5		rabid2	⊢ ( ℝ = { 𝑥 ∈ ℝ ∣ ( -∞ < 𝑥 ∧ 𝑥 < +∞ ) } ↔ ∀ 𝑥 ∈ ℝ ( -∞ < 𝑥 ∧ 𝑥 < +∞ ) )
6		mnflt	⊢ ( 𝑥 ∈ ℝ → -∞ < 𝑥 )
7		ltpnf	⊢ ( 𝑥 ∈ ℝ → 𝑥 < +∞ )
8	6 7	jca	⊢ ( 𝑥 ∈ ℝ → ( -∞ < 𝑥 ∧ 𝑥 < +∞ ) )
9	5 8	mprgbir	⊢ ℝ = { 𝑥 ∈ ℝ ∣ ( -∞ < 𝑥 ∧ 𝑥 < +∞ ) }
10	4 9	eqtr4i	⊢ ( -∞ (,) +∞ ) = ℝ