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

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 ( 𝐴 , ℝ* , < ) ∈ ℝ )