Theorem supxr2

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

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

Proof

Step	Hyp	Ref	Expression
1		ssel2	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ* )
2		xrlenlt	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑥 ≤ 𝐵 ↔ ¬ 𝐵 < 𝑥 ) )
3	1 2	sylan	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ∈ ℝ* ) → ( 𝑥 ≤ 𝐵 ↔ ¬ 𝐵 < 𝑥 ) )
4	3	an32s	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ≤ 𝐵 ↔ ¬ 𝐵 < 𝑥 ) )
5	4	ralbidva	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝐵 < 𝑥 ) )
6	5	anbi1d	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝐵 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝐵 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) ) )
7	6	biimpa	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝐵 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) ) → ( ∀ 𝑥 ∈ 𝐴 ¬ 𝐵 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) )
8		supxr	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝐵 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) ) → sup ( 𝐴 , ℝ* , < ) = 𝐵 )
9	7 8	syldan	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝐵 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) ) → sup ( 𝐴 , ℝ* , < ) = 𝐵 )