Theorem supxrleub

Description: The supremum of a set of extended reals is less than or equal to an upper bound. (Contributed by NM, 22-Feb-2006) (Revised by Mario Carneiro, 6-Sep-2014)

	Ref	Expression
Assertion	supxrleub	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( sup ( 𝐴 , ℝ* , < ) ≤ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		supxrlub	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐵 < sup ( 𝐴 , ℝ* , < ) ↔ ∃ 𝑥 ∈ 𝐴 𝐵 < 𝑥 ) )
2	1	notbid	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ¬ 𝐵 < sup ( 𝐴 , ℝ* , < ) ↔ ¬ ∃ 𝑥 ∈ 𝐴 𝐵 < 𝑥 ) )
3		ralnex	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝐵 < 𝑥 ↔ ¬ ∃ 𝑥 ∈ 𝐴 𝐵 < 𝑥 )
4	2 3	bitr4di	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ¬ 𝐵 < sup ( 𝐴 , ℝ* , < ) ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝐵 < 𝑥 ) )
5		supxrcl	⊢ ( 𝐴 ⊆ ℝ* → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
6		xrlenlt	⊢ ( ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( sup ( 𝐴 , ℝ* , < ) ≤ 𝐵 ↔ ¬ 𝐵 < sup ( 𝐴 , ℝ* , < ) ) )
7	5 6	sylan	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( sup ( 𝐴 , ℝ* , < ) ≤ 𝐵 ↔ ¬ 𝐵 < sup ( 𝐴 , ℝ* , < ) ) )
8		simpl	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) → 𝐴 ⊆ ℝ* )
9	8	sselda	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ* )
10		simplr	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
11	9 10	xrlenltd	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ≤ 𝐵 ↔ ¬ 𝐵 < 𝑥 ) )
12	11	ralbidva	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝐵 < 𝑥 ) )
13	4 7 12	3bitr4d	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( sup ( 𝐴 , ℝ* , < ) ≤ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝐵 ) )