Theorem supxrre1

Description: The supremum of a nonempty set of reals is real iff it is less than plus infinity. (Contributed by NM, 5-Feb-2006)

	Ref	Expression
Assertion	supxrre1	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ↔ sup ( 𝐴 , ℝ* , < ) < +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		supxrgtmnf	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → -∞ < sup ( 𝐴 , ℝ* , < ) )
2		ressxr	⊢ ℝ ⊆ ℝ*
3		sstr	⊢ ( ( 𝐴 ⊆ ℝ ∧ ℝ ⊆ ℝ* ) → 𝐴 ⊆ ℝ* )
4	2 3	mpan2	⊢ ( 𝐴 ⊆ ℝ → 𝐴 ⊆ ℝ* )
5		supxrcl	⊢ ( 𝐴 ⊆ ℝ* → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
6		xrrebnd	⊢ ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* → ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ↔ ( -∞ < sup ( 𝐴 , ℝ* , < ) ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) ) )
7	4 5 6	3syl	⊢ ( 𝐴 ⊆ ℝ → ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ↔ ( -∞ < sup ( 𝐴 , ℝ* , < ) ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) ) )
8	7	adantr	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ↔ ( -∞ < sup ( 𝐴 , ℝ* , < ) ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) ) )
9	1 8	mpbirand	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ↔ sup ( 𝐴 , ℝ* , < ) < +∞ ) )