Metamath Proof Explorer


Theorem supxrbnd

Description: The supremum of a bounded-above nonempty set of reals is real. (Contributed by NM, 19-Jan-2006)

Ref Expression
Assertion supxrbnd ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 ressxr ℝ ⊆ ℝ*
2 sstr ( ( 𝐴 ⊆ ℝ ∧ ℝ ⊆ ℝ* ) → 𝐴 ⊆ ℝ* )
3 1 2 mpan2 ( 𝐴 ⊆ ℝ → 𝐴 ⊆ ℝ* )
4 supxrcl ( 𝐴 ⊆ ℝ* → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
5 pnfxr +∞ ∈ ℝ*
6 xrltne ( ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) → +∞ ≠ sup ( 𝐴 , ℝ* , < ) )
7 5 6 mp3an2 ( ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) → +∞ ≠ sup ( 𝐴 , ℝ* , < ) )
8 7 necomd ( ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) → sup ( 𝐴 , ℝ* , < ) ≠ +∞ )
9 8 ex ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* → ( sup ( 𝐴 , ℝ* , < ) < +∞ → sup ( 𝐴 , ℝ* , < ) ≠ +∞ ) )
10 4 9 syl ( 𝐴 ⊆ ℝ* → ( sup ( 𝐴 , ℝ* , < ) < +∞ → sup ( 𝐴 , ℝ* , < ) ≠ +∞ ) )
11 supxrunb2 ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦𝐴 𝑥 < 𝑦 ↔ sup ( 𝐴 , ℝ* , < ) = +∞ ) )
12 ssel2 ( ( 𝐴 ⊆ ℝ*𝑦𝐴 ) → 𝑦 ∈ ℝ* )
13 12 adantlr ( ( ( 𝐴 ⊆ ℝ*𝑥 ∈ ℝ ) ∧ 𝑦𝐴 ) → 𝑦 ∈ ℝ* )
14 rexr ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
15 14 ad2antlr ( ( ( 𝐴 ⊆ ℝ*𝑥 ∈ ℝ ) ∧ 𝑦𝐴 ) → 𝑥 ∈ ℝ* )
16 xrlenlt ( ( 𝑦 ∈ ℝ*𝑥 ∈ ℝ* ) → ( 𝑦𝑥 ↔ ¬ 𝑥 < 𝑦 ) )
17 16 con2bid ( ( 𝑦 ∈ ℝ*𝑥 ∈ ℝ* ) → ( 𝑥 < 𝑦 ↔ ¬ 𝑦𝑥 ) )
18 13 15 17 syl2anc ( ( ( 𝐴 ⊆ ℝ*𝑥 ∈ ℝ ) ∧ 𝑦𝐴 ) → ( 𝑥 < 𝑦 ↔ ¬ 𝑦𝑥 ) )
19 18 rexbidva ( ( 𝐴 ⊆ ℝ*𝑥 ∈ ℝ ) → ( ∃ 𝑦𝐴 𝑥 < 𝑦 ↔ ∃ 𝑦𝐴 ¬ 𝑦𝑥 ) )
20 rexnal ( ∃ 𝑦𝐴 ¬ 𝑦𝑥 ↔ ¬ ∀ 𝑦𝐴 𝑦𝑥 )
21 19 20 bitrdi ( ( 𝐴 ⊆ ℝ*𝑥 ∈ ℝ ) → ( ∃ 𝑦𝐴 𝑥 < 𝑦 ↔ ¬ ∀ 𝑦𝐴 𝑦𝑥 ) )
22 21 ralbidva ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦𝐴 𝑥 < 𝑦 ↔ ∀ 𝑥 ∈ ℝ ¬ ∀ 𝑦𝐴 𝑦𝑥 ) )
23 11 22 bitr3d ( 𝐴 ⊆ ℝ* → ( sup ( 𝐴 , ℝ* , < ) = +∞ ↔ ∀ 𝑥 ∈ ℝ ¬ ∀ 𝑦𝐴 𝑦𝑥 ) )
24 ralnex ( ∀ 𝑥 ∈ ℝ ¬ ∀ 𝑦𝐴 𝑦𝑥 ↔ ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 )
25 23 24 bitrdi ( 𝐴 ⊆ ℝ* → ( sup ( 𝐴 , ℝ* , < ) = +∞ ↔ ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 ) )
26 25 necon2abid ( 𝐴 ⊆ ℝ* → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 ↔ sup ( 𝐴 , ℝ* , < ) ≠ +∞ ) )
27 10 26 sylibrd ( 𝐴 ⊆ ℝ* → ( sup ( 𝐴 , ℝ* , < ) < +∞ → ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 ) )
28 27 imp ( ( 𝐴 ⊆ ℝ* ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 )
29 3 28 sylan ( ( 𝐴 ⊆ ℝ ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 )
30 29 3adant2 ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 )
31 supxrre ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 ) → sup ( 𝐴 , ℝ* , < ) = sup ( 𝐴 , ℝ , < ) )
32 suprcl ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 ) → sup ( 𝐴 , ℝ , < ) ∈ ℝ )
33 31 32 eqeltrd ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ )
34 30 33 syld3an3 ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ )