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	syl6rbb	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) → ( ¬ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) )
11	10	ralbidva	⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ¬ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) )
12	1 11	syl5bbr	⊢ ( 𝐴 ⊆ ℝ* → ( ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) )
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 ( 𝐴 , ℝ* , < ) < +∞ ) )