Theorem supxrre2

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

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

Proof

Step	Hyp	Ref	Expression
1		supxrre1	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ↔ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
2		ressxr	⊢ ℝ ⊆ ℝ*
3		sstr	⊢ ( ( 𝐴 ⊆ ℝ ∧ ℝ ⊆ ℝ* ) → 𝐴 ⊆ ℝ* )
4	2 3	mpan2	⊢ ( 𝐴 ⊆ ℝ → 𝐴 ⊆ ℝ* )
5		supxrcl	⊢ ( 𝐴 ⊆ ℝ* → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
6		nltpnft	⊢ ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* → ( sup ( 𝐴 , ℝ* , < ) = +∞ ↔ ¬ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
7	4 5 6	3syl	⊢ ( 𝐴 ⊆ ℝ → ( sup ( 𝐴 , ℝ* , < ) = +∞ ↔ ¬ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
8	7	necon2abid	⊢ ( 𝐴 ⊆ ℝ → ( sup ( 𝐴 , ℝ* , < ) < +∞ ↔ sup ( 𝐴 , ℝ* , < ) ≠ +∞ ) )
9	8	adantr	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( sup ( 𝐴 , ℝ* , < ) < +∞ ↔ sup ( 𝐴 , ℝ* , < ) ≠ +∞ ) )
10	1 9	bitrd	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ↔ sup ( 𝐴 , ℝ* , < ) ≠ +∞ ) )