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

Metamath Proof Explorer

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 ( 𝐴 , ℝ^* , < ) = 𝐵 )