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	$⊢ (A \subseteq ℝ^{} \land +∞ \in A) \to sup (A ℝ^{} <) = +∞$

Step	Hyp	Ref	Expression
1		ssel	$⊢ A \subseteq ℝ^{} \to (y \in A \to y \in ℝ^{})$
2		pnfnlt	$⊢ y \in ℝ^{*} \to \neg +∞ < y$
3	1 2	syl6	$⊢ A \subseteq ℝ^{*} \to (y \in A \to \neg +∞ < y)$
4	3	ralrimiv	$⊢ A \subseteq ℝ^{*} \to \forall y \in A \neg +∞ < y$
5		breq2	$⊢ z = +∞ \to (y < z \leftrightarrow y < +∞)$
6	5	rspcev	$⊢ (+∞ \in A \land y < +∞) \to \exists z \in A y < z$
7	6	ex	$⊢ +∞ \in A \to (y < +∞ \to \exists z \in A y < z)$
8	7	ralrimivw	$⊢ +∞ \in A \to \forall y \in ℝ (y < +∞ \to \exists z \in A y < z)$
9	4 8	anim12i	$⊢ (A \subseteq ℝ^{*} \land +∞ \in A) \to (\forall y \in A \neg +∞ < y \land \forall y \in ℝ (y < +∞ \to \exists z \in A y < z))$
10		pnfxr	$⊢ +∞ \in ℝ^{*}$
11		supxr	$⊢ ((A \subseteq ℝ^{} \land +∞ \in ℝ^{}) \land (\forall y \in A \neg +∞ < y \land \forall y \in ℝ (y < +∞ \to \exists z \in A y < z))) \to sup (A ℝ^{*} <) = +∞$
12	10 11	mpanl2	$⊢ (A \subseteq ℝ^{} \land (\forall y \in A \neg +∞ < y \land \forall y \in ℝ (y < +∞ \to \exists z \in A y < z))) \to sup (A ℝ^{} <) = +∞$
13	9 12	syldan	$⊢ (A \subseteq ℝ^{} \land +∞ \in A) \to sup (A ℝ^{} <) = +∞$

Metamath Proof Explorer