Metamath Proof Explorer


Theorem supxrbnd1

Description: The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006)

Ref Expression
Assertion supxrbnd1 ( 𝐴 ⊆ ℝ* → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦 < 𝑥 ↔ sup ( 𝐴 , ℝ* , < ) < +∞ ) )

Proof

Step Hyp Ref Expression
1 ralnex ( ∀ 𝑥 ∈ ℝ ¬ ∀ 𝑦𝐴 𝑦 < 𝑥 ↔ ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦 < 𝑥 )
2 rexr ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
3 ssel2 ( ( 𝐴 ⊆ ℝ*𝑦𝐴 ) → 𝑦 ∈ ℝ* )
4 xrlenlt ( ( 𝑥 ∈ ℝ*𝑦 ∈ ℝ* ) → ( 𝑥𝑦 ↔ ¬ 𝑦 < 𝑥 ) )
5 2 3 4 syl2anr ( ( ( 𝐴 ⊆ ℝ*𝑦𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥𝑦 ↔ ¬ 𝑦 < 𝑥 ) )
6 5 an32s ( ( ( 𝐴 ⊆ ℝ*𝑥 ∈ ℝ ) ∧ 𝑦𝐴 ) → ( 𝑥𝑦 ↔ ¬ 𝑦 < 𝑥 ) )
7 6 rexbidva ( ( 𝐴 ⊆ ℝ*𝑥 ∈ ℝ ) → ( ∃ 𝑦𝐴 𝑥𝑦 ↔ ∃ 𝑦𝐴 ¬ 𝑦 < 𝑥 ) )
8 rexnal ( ∃ 𝑦𝐴 ¬ 𝑦 < 𝑥 ↔ ¬ ∀ 𝑦𝐴 𝑦 < 𝑥 )
9 7 8 bitr2di ( ( 𝐴 ⊆ ℝ*𝑥 ∈ ℝ ) → ( ¬ ∀ 𝑦𝐴 𝑦 < 𝑥 ↔ ∃ 𝑦𝐴 𝑥𝑦 ) )
10 9 ralbidva ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ¬ ∀ 𝑦𝐴 𝑦 < 𝑥 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑦𝐴 𝑥𝑦 ) )
11 1 10 bitr3id ( 𝐴 ⊆ ℝ* → ( ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦 < 𝑥 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑦𝐴 𝑥𝑦 ) )
12 supxrunb1 ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦𝐴 𝑥𝑦 ↔ sup ( 𝐴 , ℝ* , < ) = +∞ ) )
13 supxrcl ( 𝐴 ⊆ ℝ* → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
14 nltpnft ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* → ( sup ( 𝐴 , ℝ* , < ) = +∞ ↔ ¬ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
15 13 14 syl ( 𝐴 ⊆ ℝ* → ( sup ( 𝐴 , ℝ* , < ) = +∞ ↔ ¬ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
16 11 12 15 3bitrd ( 𝐴 ⊆ ℝ* → ( ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦 < 𝑥 ↔ ¬ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
17 16 con4bid ( 𝐴 ⊆ ℝ* → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦 < 𝑥 ↔ sup ( 𝐴 , ℝ* , < ) < +∞ ) )