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

Metamath Proof Explorer

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 ( 𝐴 , ℝ^* , < ) ≤ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝐵 ) )