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

Metamath Proof Explorer

Theorem suprlub

Description: The supremum of a nonempty bounded set of reals is the least upper bound. (Contributed by NM, 15-Nov-2004) (Revised by Mario Carneiro, 6-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		ltso	⊢ < Or ℝ
2	1	a1i	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → < Or ℝ )
3		sup3	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑤 ∈ 𝐴 𝑦 < 𝑤 ) ) )
4		simp1	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → 𝐴 ⊆ ℝ )
5	2 3 4	suplub2	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝐵 ∈ ℝ ) → ( 𝐵 < sup ( 𝐴 , ℝ , < ) ↔ ∃ 𝑤 ∈ 𝐴 𝐵 < 𝑤 ) )
6		breq2	⊢ ( 𝑤 = 𝑧 → ( 𝐵 < 𝑤 ↔ 𝐵 < 𝑧 ) )
7	6	cbvrexvw	⊢ ( ∃ 𝑤 ∈ 𝐴 𝐵 < 𝑤 ↔ ∃ 𝑧 ∈ 𝐴 𝐵 < 𝑧 )
8	5 7	bitrdi	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝐵 ∈ ℝ ) → ( 𝐵 < sup ( 𝐴 , ℝ , < ) ↔ ∃ 𝑧 ∈ 𝐴 𝐵 < 𝑧 ) )