icopnfsup

Description: An upper set of reals is unbounded above. (Contributed by Mario Carneiro, 7-May-2016)

		Ref	Expression
	Assertion	icopnfsup	$⊢ (A \in ℝ^{} \land A \neq +∞) \to sup ([A, +∞) ℝ^{} <) = +∞$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in ℝ^{} \land A \neq +∞) \to A \in ℝ^{}$
2		pnfxr	$⊢ +∞ \in ℝ^{*}$
3	2	a1i	$⊢ (A \in ℝ^{} \land A \neq +∞) \to +∞ \in ℝ^{}$
4		nltpnft	$⊢ A \in ℝ^{*} \to (A = +∞ \leftrightarrow \neg A < +∞)$
5	4	necon2abid	$⊢ A \in ℝ^{*} \to (A < +∞ \leftrightarrow A \neq +∞)$
6	5	biimpar	$⊢ (A \in ℝ^{*} \land A \neq +∞) \to A < +∞$
7		lbico1	$⊢ (A \in ℝ^{} \land +∞ \in ℝ^{} \land A < +∞) \to A \in [A, +∞)$
8	1 3 6 7	syl3anc	$⊢ (A \in ℝ^{*} \land A \neq +∞) \to A \in [A, +∞)$
9	8	ne0d	$⊢ (A \in ℝ^{*} \land A \neq +∞) \to [A, +∞) \neq \emptyset$
10		df-ico	$⊢ [.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
11		idd	$⊢ (w \in ℝ^{} \land +∞ \in ℝ^{}) \to (w < +∞ \to w < +∞)$
12		xrltle	$⊢ (w \in ℝ^{} \land +∞ \in ℝ^{}) \to (w < +∞ \to w \leq +∞)$
13		xrltle	$⊢ (A \in ℝ^{} \land w \in ℝ^{}) \to (A < w \to A \leq w)$
14		idd	$⊢ (A \in ℝ^{} \land w \in ℝ^{}) \to (A \leq w \to A \leq w)$
15	10 11 12 13 14	ixxub	$⊢ (A \in ℝ^{} \land +∞ \in ℝ^{} \land [A, +∞) \neq \emptyset) \to sup ([A, +∞) ℝ^{*} <) = +∞$
16	1 3 9 15	syl3anc	$⊢ (A \in ℝ^{} \land A \neq +∞) \to sup ([A, +∞) ℝ^{} <) = +∞$

Metamath Proof Explorer