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

Metamath Proof Explorer

Theorem lbreu

Description: If a set of reals contains a lower bound, it contains a unique lower bound. (Contributed by NM, 9-Oct-2005)

Ref Expression
Assertion lbreu ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) → ∃! 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 )

Proof

Step Hyp Ref Expression
1 breq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑥 ≤ 𝑦 ↔ 𝑥 ≤ 𝑤 ) )
2 1 rspcv ⊢ ( 𝑤 ∈ 𝑆 → ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑥 ≤ 𝑤 ) )
3 breq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑤 ≤ 𝑦 ↔ 𝑤 ≤ 𝑥 ) )
4 3 rspcv ⊢ ( 𝑥 ∈ 𝑆 → ( ∀ 𝑦 ∈ 𝑆 𝑤 ≤ 𝑦 → 𝑤 ≤ 𝑥 ) )
5 2 4 im2anan9r ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) → ( ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑦 ∈ 𝑆 𝑤 ≤ 𝑦 ) → ( 𝑥 ≤ 𝑤 ∧ 𝑤 ≤ 𝑥 ) ) )
6 ssel ⊢ ( 𝑆 ⊆ ℝ → ( 𝑥 ∈ 𝑆 → 𝑥 ∈ ℝ ) )
7 ssel ⊢ ( 𝑆 ⊆ ℝ → ( 𝑤 ∈ 𝑆 → 𝑤 ∈ ℝ ) )
8 6 7 anim12d ⊢ ( 𝑆 ⊆ ℝ → ( ( 𝑥 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) → ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ ℝ ) ) )
9 8 impcom ⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑆 ⊆ ℝ ) → ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ ℝ ) )
10 letri3 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ ℝ ) → ( 𝑥 = 𝑤 ↔ ( 𝑥 ≤ 𝑤 ∧ 𝑤 ≤ 𝑥 ) ) )
11 9 10 syl ⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑆 ⊆ ℝ ) → ( 𝑥 = 𝑤 ↔ ( 𝑥 ≤ 𝑤 ∧ 𝑤 ≤ 𝑥 ) ) )
12 11 exbiri ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) → ( 𝑆 ⊆ ℝ → ( ( 𝑥 ≤ 𝑤 ∧ 𝑤 ≤ 𝑥 ) → 𝑥 = 𝑤 ) ) )
13 12 com23 ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝑥 ≤ 𝑤 ∧ 𝑤 ≤ 𝑥 ) → ( 𝑆 ⊆ ℝ → 𝑥 = 𝑤 ) ) )
14 5 13 syld ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) → ( ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑦 ∈ 𝑆 𝑤 ≤ 𝑦 ) → ( 𝑆 ⊆ ℝ → 𝑥 = 𝑤 ) ) )
15 14 com3r ⊢ ( 𝑆 ⊆ ℝ → ( ( 𝑥 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) → ( ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑦 ∈ 𝑆 𝑤 ≤ 𝑦 ) → 𝑥 = 𝑤 ) ) )
16 15 ralrimivv ⊢ ( 𝑆 ⊆ ℝ → ∀ 𝑥 ∈ 𝑆 ∀ 𝑤 ∈ 𝑆 ( ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑦 ∈ 𝑆 𝑤 ≤ 𝑦 ) → 𝑥 = 𝑤 ) )
17 16 anim1ci ⊢ ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) → ( ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑤 ∈ 𝑆 ( ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑦 ∈ 𝑆 𝑤 ≤ 𝑦 ) → 𝑥 = 𝑤 ) ) )
18 breq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 ≤ 𝑦 ↔ 𝑤 ≤ 𝑦 ) )
19 18 ralbidv ⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ↔ ∀ 𝑦 ∈ 𝑆 𝑤 ≤ 𝑦 ) )
20 19 reu4 ⊢ ( ∃! 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ↔ ( ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑤 ∈ 𝑆 ( ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑦 ∈ 𝑆 𝑤 ≤ 𝑦 ) → 𝑥 = 𝑤 ) ) )
21 17 20 sylibr ⊢ ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) → ∃! 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 )