Theorem supxr

Description: The supremum of a set of extended reals. (Contributed by NM, 9-Apr-2006) (Revised by Mario Carneiro, 21-Apr-2015)

	Ref	Expression
Assertion	supxr	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝐵 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) ) → sup ( 𝐴 , ℝ* , < ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		simplr	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝐵 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) ) → 𝐵 ∈ ℝ* )
2		simprl	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝐵 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝐴 ¬ 𝐵 < 𝑥 )
3		xrub	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ↔ ∀ 𝑥 ∈ ℝ* ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) )
4	3	biimpa	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) → ∀ 𝑥 ∈ ℝ* ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) )
5	4	adantrl	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝐵 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) ) → ∀ 𝑥 ∈ ℝ* ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) )
6		xrltso	⊢ < Or ℝ*
7	6	a1i	⊢ ( ⊤ → < Or ℝ* )
8	7	eqsup	⊢ ( ⊤ → ( ( 𝐵 ∈ ℝ* ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝐵 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ* ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) → sup ( 𝐴 , ℝ* , < ) = 𝐵 ) )
9	8	mptru	⊢ ( ( 𝐵 ∈ ℝ* ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝐵 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ* ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) → sup ( 𝐴 , ℝ* , < ) = 𝐵 )
10	1 2 5 9	syl3anc	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝐵 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) ) → sup ( 𝐴 , ℝ* , < ) = 𝐵 )