Metamath Proof Explorer

Theorem suprleub

Description: The supremum of a nonempty bounded set of reals is less than or equal to an upper bound. (Contributed by NM, 18-Mar-2005) (Revised by Mario Carneiro, 6-Sep-2014)

Ref Expression
Assertion suprleub ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧B∈ℝ→supAℝ<≤B↔∀z∈Az≤B

Proof

Step Hyp Ref Expression
1 suprnub ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧B∈ℝ→¬B<supAℝ<↔∀w∈A¬B<w
2 suprcl ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x→supAℝ<∈ℝ
3 lenlt ⊢supAℝ<∈ℝ∧B∈ℝ→supAℝ<≤B↔¬B<supAℝ<
4 2 3 sylan ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧B∈ℝ→supAℝ<≤B↔¬B<supAℝ<
5 simpl1 ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧B∈ℝ→A⊆ℝ
6 5 sselda ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧B∈ℝ∧w∈A→w∈ℝ
7 simplr ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧B∈ℝ∧w∈A→B∈ℝ
8 6 7 lenltd ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧B∈ℝ∧w∈A→w≤B↔¬B<w
9 8 ralbidva ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧B∈ℝ→∀w∈Aw≤B↔∀w∈A¬B<w
10 1 4 9 3bitr4d ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧B∈ℝ→supAℝ<≤B↔∀w∈Aw≤B
11 breq1 ⊢w=z→w≤B↔z≤B
12 11 cbvralvw ⊢∀w∈Aw≤B↔∀z∈Az≤B
13 10 12 bitrdi ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧B∈ℝ→supAℝ<≤B↔∀z∈Az≤B