ioopnfsup

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

		Ref	Expression
	Assertion	ioopnfsup	$⊢ (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		ioon0	$⊢ (A \in ℝ^{} \land +∞ \in ℝ^{}) \to ((A, +∞) \neq \emptyset \leftrightarrow A < +∞)$
8	3 7	syldan	$⊢ (A \in ℝ^{*} \land A \neq +∞) \to ((A, +∞) \neq \emptyset \leftrightarrow A < +∞)$
9	6 8	mpbird	$⊢ (A \in ℝ^{*} \land A \neq +∞) \to (A, +∞) \neq \emptyset$
10		df-ioo	$⊢ (.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < 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		idd	$⊢ (A \in ℝ^{} \land w \in ℝ^{}) \to (A < w \to A < w)$
14		xrltle	$⊢ (A \in ℝ^{} \land w \in ℝ^{}) \to (A < 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