Metamath Proof Explorer

Theorem supxr2

Description: The supremum of a set of extended reals. (Contributed by NM, 9-Apr-2006)

Ref Expression
Assertion supxr2 ⊢A⊆ℝ*∧B∈ℝ*∧∀x∈Ax≤B∧∀x∈ℝx<B→∃y∈Ax<y→supAℝ*<=B

Proof

Step Hyp Ref Expression
1 ssel2 ⊢A⊆ℝ*∧x∈A→x∈ℝ*
2 xrlenlt ⊢x∈ℝ*∧B∈ℝ*→x≤B↔¬B<x
3 1 2 sylan ⊢A⊆ℝ*∧x∈A∧B∈ℝ*→x≤B↔¬B<x
4 3 an32s ⊢A⊆ℝ*∧B∈ℝ*∧x∈A→x≤B↔¬B<x
5 4 ralbidva ⊢A⊆ℝ*∧B∈ℝ*→∀x∈Ax≤B↔∀x∈A¬B<x
6 5 anbi1d ⊢A⊆ℝ*∧B∈ℝ*→∀x∈Ax≤B∧∀x∈ℝx<B→∃y∈Ax<y↔∀x∈A¬B<x∧∀x∈ℝx<B→∃y∈Ax<y
7 6 biimpa ⊢A⊆ℝ*∧B∈ℝ*∧∀x∈Ax≤B∧∀x∈ℝx<B→∃y∈Ax<y→∀x∈A¬B<x∧∀x∈ℝx<B→∃y∈Ax<y
8 supxr ⊢A⊆ℝ*∧B∈ℝ*∧∀x∈A¬B<x∧∀x∈ℝx<B→∃y∈Ax<y→supAℝ*<=B
9 7 8 syldan ⊢A⊆ℝ*∧B∈ℝ*∧∀x∈Ax≤B∧∀x∈ℝx<B→∃y∈Ax<y→supAℝ*<=B