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

Metamath Proof Explorer

Theorem lble

Description: If a set of reals contains a lower bound, the lower bound is less than or equal to all members of the set. (Contributed by NM, 9-Oct-2005) (Proof shortened by Mario Carneiro, 24-Dec-2016)

Ref Expression
Assertion lble ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝐴 )

Proof

Step Hyp Ref Expression
1 lbreu ⊢ ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) → ∃! 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 )
2 nfcv ⊢ Ⅎ 𝑥 𝑆
3 nfriota1 ⊢ Ⅎ 𝑥 ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 )
4 nfcv ⊢ Ⅎ 𝑥 ≤
5 nfcv ⊢ Ⅎ 𝑥 𝑦
6 3 4 5 nfbr ⊢ Ⅎ 𝑥 ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝑦
7 2 6 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ 𝑆 ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝑦
8 eqid ⊢ ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) = ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 )
9 nfra1 ⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦
10 nfcv ⊢ Ⅎ 𝑦 𝑆
11 9 10 nfriota ⊢ Ⅎ 𝑦 ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 )
12 11 nfeq2 ⊢ Ⅎ 𝑦 𝑥 = ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 )
13 breq1 ⊢ ( 𝑥 = ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) → ( 𝑥 ≤ 𝑦 ↔ ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝑦 ) )
14 12 13 ralbid ⊢ ( 𝑥 = ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) → ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ↔ ∀ 𝑦 ∈ 𝑆 ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝑦 ) )
15 7 8 14 riotaprop ⊢ ( ∃! 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 → ( ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝑦 ) )
16 1 15 syl ⊢ ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) → ( ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝑦 ) )
17 16 simprd ⊢ ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) → ∀ 𝑦 ∈ 𝑆 ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝑦 )
18 nfcv ⊢ Ⅎ 𝑦 ≤
19 nfcv ⊢ Ⅎ 𝑦 𝐴
20 11 18 19 nfbr ⊢ Ⅎ 𝑦 ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝐴
21 breq2 ⊢ ( 𝑦 = 𝐴 → ( ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝑦 ↔ ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝐴 ) )
22 20 21 rspc ⊢ ( 𝐴 ∈ 𝑆 → ( ∀ 𝑦 ∈ 𝑆 ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝑦 → ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝐴 ) )
23 17 22 mpan9 ⊢ ( ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ∧ 𝐴 ∈ 𝑆 ) → ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝐴 )
24 23 3impa ⊢ ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝐴 )