xrsupexmnf

Description: Adding minus infinity to a set does not affect the existence of its supremum. (Contributed by NM, 26-Oct-2005)

		Ref	Expression
	Assertion	xrsupexmnf	$⊢ \exists x \in ℝ^{} (\forall y \in A \neg x < y \land \forall y \in ℝ^{} (y < x \to \exists z \in A y < z)) \to \exists x \in ℝ^{} (\forall y \in (A \cup \{−∞\}) \neg x < y \land \forall y \in ℝ^{} (y < x \to \exists z \in (A \cup \{−∞\}) y < z))$

Proof

Step	Hyp	Ref	Expression
1		elun	$⊢ y \in (A \cup \{−∞\}) \leftrightarrow (y \in A \lor y \in \{−∞\})$
2		simpr	$⊢ (x \in ℝ^{*} \land (y \in A \to \neg x < y)) \to (y \in A \to \neg x < y)$
3		velsn	$⊢ y \in \{−∞\} \leftrightarrow y = −∞$
4		nltmnf	$⊢ x \in ℝ^{*} \to \neg x < −∞$
5		breq2	$⊢ y = −∞ \to (x < y \leftrightarrow x < −∞)$
6	5	notbid	$⊢ y = −∞ \to (\neg x < y \leftrightarrow \neg x < −∞)$
7	4 6	syl5ibrcom	$⊢ x \in ℝ^{*} \to (y = −∞ \to \neg x < y)$
8	3 7	biimtrid	$⊢ x \in ℝ^{*} \to (y \in \{−∞\} \to \neg x < y)$
9	8	adantr	$⊢ (x \in ℝ^{*} \land (y \in A \to \neg x < y)) \to (y \in \{−∞\} \to \neg x < y)$
10	2 9	jaod	$⊢ (x \in ℝ^{*} \land (y \in A \to \neg x < y)) \to ((y \in A \lor y \in \{−∞\}) \to \neg x < y)$
11	1 10	biimtrid	$⊢ (x \in ℝ^{*} \land (y \in A \to \neg x < y)) \to (y \in (A \cup \{−∞\}) \to \neg x < y)$
12	11	ex	$⊢ x \in ℝ^{*} \to ((y \in A \to \neg x < y) \to (y \in (A \cup \{−∞\}) \to \neg x < y))$
13	12	ralimdv2	$⊢ x \in ℝ^{*} \to (\forall y \in A \neg x < y \to \forall y \in (A \cup \{−∞\}) \neg x < y)$
14		elun1	$⊢ z \in A \to z \in (A \cup \{−∞\})$
15	14	anim1i	$⊢ (z \in A \land y < z) \to (z \in (A \cup \{−∞\}) \land y < z)$
16	15	reximi2	$⊢ \exists z \in A y < z \to \exists z \in (A \cup \{−∞\}) y < z$
17	16	imim2i	$⊢ (y < x \to \exists z \in A y < z) \to (y < x \to \exists z \in (A \cup \{−∞\}) y < z)$
18	17	ralimi	$⊢ \forall y \in ℝ^{} (y < x \to \exists z \in A y < z) \to \forall y \in ℝ^{} (y < x \to \exists z \in (A \cup \{−∞\}) y < z)$
19	13 18	anim12d1	$⊢ x \in ℝ^{} \to ((\forall y \in A \neg x < y \land \forall y \in ℝ^{} (y < x \to \exists z \in A y < z)) \to (\forall y \in (A \cup \{−∞\}) \neg x < y \land \forall y \in ℝ^{*} (y < x \to \exists z \in (A \cup \{−∞\}) y < z)))$
20	19	reximia	$⊢ \exists x \in ℝ^{} (\forall y \in A \neg x < y \land \forall y \in ℝ^{} (y < x \to \exists z \in A y < z)) \to \exists x \in ℝ^{} (\forall y \in (A \cup \{−∞\}) \neg x < y \land \forall y \in ℝ^{} (y < x \to \exists z \in (A \cup \{−∞\}) y < z))$

Metamath Proof Explorer

Theorem xrsupexmnf

Proof