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

Metamath Proof Explorer

Theorem supxrpnf

Description: The supremum of a set of extended reals containing plus infinity is plus infinity. (Contributed by NM, 15-Oct-2005)

Ref Expression
Assertion supxrpnf ( ( 𝐴 ⊆ ℝ* ∧ +∞ ∈ 𝐴 ) → sup ( 𝐴 , ℝ* , < ) = +∞ )

Proof

Step Hyp Ref Expression
1 ssel ⊢ ( 𝐴 ⊆ ℝ* → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℝ* ) )
2 pnfnlt ⊢ ( 𝑦 ∈ ℝ* → ¬ +∞ < 𝑦 )
3 1 2 syl6 ⊢ ( 𝐴 ⊆ ℝ* → ( 𝑦 ∈ 𝐴 → ¬ +∞ < 𝑦 ) )
4 3 ralrimiv ⊢ ( 𝐴 ⊆ ℝ* → ∀ 𝑦 ∈ 𝐴 ¬ +∞ < 𝑦 )
5 breq2 ⊢ ( 𝑧 = +∞ → ( 𝑦 < 𝑧 ↔ 𝑦 < +∞ ) )
6 5 rspcev ⊢ ( ( +∞ ∈ 𝐴 ∧ 𝑦 < +∞ ) → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 )
7 6 ex ⊢ ( +∞ ∈ 𝐴 → ( 𝑦 < +∞ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) )
8 7 ralrimivw ⊢ ( +∞ ∈ 𝐴 → ∀ 𝑦 ∈ ℝ ( 𝑦 < +∞ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) )
9 4 8 anim12i ⊢ ( ( 𝐴 ⊆ ℝ* ∧ +∞ ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ¬ +∞ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < +∞ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
10 pnfxr ⊢ +∞ ∈ ℝ*
11 supxr ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ +∞ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < +∞ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) → sup ( 𝐴 , ℝ* , < ) = +∞ )
12 10 11 mpanl2 ⊢ ( ( 𝐴 ⊆ ℝ* ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ +∞ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < +∞ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) → sup ( 𝐴 , ℝ* , < ) = +∞ )
13 9 12 syldan ⊢ ( ( 𝐴 ⊆ ℝ* ∧ +∞ ∈ 𝐴 ) → sup ( 𝐴 , ℝ* , < ) = +∞ )