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

Metamath Proof Explorer

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