Metamath Proof Explorer


Theorem supxrbnd2

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

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

Proof

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