This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝐴 , ℝ^* , < ) ∈ ℝ ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) )