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 ( 𝐴 , ℝ* , < ) = +∞ )