Theorem supxrre3

Description: The supremum of a nonempty set of reals, is real if and only if it is bounded-above . (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	supxrre3	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		supxrre1	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ↔ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
2		id	⊢ ( 𝐴 ⊆ ℝ → 𝐴 ⊆ ℝ )
3		rexr	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
4	3	ssriv	⊢ ℝ ⊆ ℝ*
5	4	a1i	⊢ ( 𝐴 ⊆ ℝ → ℝ ⊆ ℝ* )
6	2 5	sstrd	⊢ ( 𝐴 ⊆ ℝ → 𝐴 ⊆ ℝ* )
7		supxrbnd2	⊢ ( 𝐴 ⊆ ℝ* → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
8	6 7	syl	⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
9	8	bicomd	⊢ ( 𝐴 ⊆ ℝ → ( sup ( 𝐴 , ℝ* , < ) < +∞ ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) )
10	9	adantr	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( sup ( 𝐴 , ℝ* , < ) < +∞ ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) )
11	1 10	bitrd	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) )