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

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