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

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 ( 𝐴 , ℝ^* , < ) < +∞ ) )