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 ⊢S⊆ℝ∧∃x∈S∀y∈Sx≤y∧A∈S→ιx∈S|∀y∈Sx≤y≤A

Proof

Step Hyp Ref Expression
1 lbreu ⊢S⊆ℝ∧∃x∈S∀y∈Sx≤y→∃!x∈S∀y∈Sx≤y
2 nfcv ⊢Ⅎ_xS
3 nfriota1 ⊢Ⅎ_xιx∈S|∀y∈Sx≤y
4 nfcv ⊢Ⅎ_x≤
5 nfcv ⊢Ⅎ_xy
6 3 4 5 nfbr ⊢Ⅎxιx∈S|∀y∈Sx≤y≤y
7 2 6 nfralw ⊢Ⅎx∀y∈Sιx∈S|∀y∈Sx≤y≤y
8 eqid ⊢ιx∈S|∀y∈Sx≤y=ιx∈S|∀y∈Sx≤y
9 nfra1 ⊢Ⅎy∀y∈Sx≤y
10 nfcv ⊢Ⅎ_yS
11 9 10 nfriota ⊢Ⅎ_yιx∈S|∀y∈Sx≤y
12 11 nfeq2 ⊢Ⅎyx=ιx∈S|∀y∈Sx≤y
13 breq1 ⊢x=ιx∈S|∀y∈Sx≤y→x≤y↔ιx∈S|∀y∈Sx≤y≤y
14 12 13 ralbid ⊢x=ιx∈S|∀y∈Sx≤y→∀y∈Sx≤y↔∀y∈Sιx∈S|∀y∈Sx≤y≤y
15 7 8 14 riotaprop ⊢∃!x∈S∀y∈Sx≤y→ιx∈S|∀y∈Sx≤y∈S∧∀y∈Sιx∈S|∀y∈Sx≤y≤y
16 1 15 syl ⊢S⊆ℝ∧∃x∈S∀y∈Sx≤y→ιx∈S|∀y∈Sx≤y∈S∧∀y∈Sιx∈S|∀y∈Sx≤y≤y
17 16 simprd ⊢S⊆ℝ∧∃x∈S∀y∈Sx≤y→∀y∈Sιx∈S|∀y∈Sx≤y≤y
18 nfcv ⊢Ⅎ_y≤
19 nfcv ⊢Ⅎ_yA
20 11 18 19 nfbr ⊢Ⅎyιx∈S|∀y∈Sx≤y≤A
21 breq2 ⊢y=A→ιx∈S|∀y∈Sx≤y≤y↔ιx∈S|∀y∈Sx≤y≤A
22 20 21 rspc ⊢A∈S→∀y∈Sιx∈S|∀y∈Sx≤y≤y→ιx∈S|∀y∈Sx≤y≤A
23 17 22 mpan9 ⊢S⊆ℝ∧∃x∈S∀y∈Sx≤y∧A∈S→ιx∈S|∀y∈Sx≤y≤A
24 23 3impa ⊢S⊆ℝ∧∃x∈S∀y∈Sx≤y∧A∈S→ιx∈S|∀y∈Sx≤y≤A