xrsupss

Description: Any subset of extended reals has a supremum. (Contributed by NM, 25-Oct-2005)

		Ref	Expression
	Assertion	xrsupss	$⊢ A \subseteq ℝ^{} \to \exists x \in ℝ^{} (\forall y \in A \neg x < y \land \forall y \in ℝ^{*} (y < x \to \exists z \in A y < z))$

Proof

Step	Hyp	Ref	Expression
1		xrsupsslem	$⊢ (A \subseteq ℝ^{} \land (A \subseteq ℝ \lor +∞ \in A)) \to \exists x \in ℝ^{} (\forall y \in A \neg x < y \land \forall y \in ℝ^{*} (y < x \to \exists z \in A y < z))$
2		ssdifss	$⊢ A \subseteq ℝ^{} \to A ∖ \{−∞\} \subseteq ℝ^{}$
3		ssxr	$⊢ A ∖ \{−∞\} \subseteq ℝ^{*} \to (A ∖ \{−∞\} \subseteq ℝ \lor +∞ \in (A ∖ \{−∞\}) \lor −∞ \in (A ∖ \{−∞\}))$
4		df-3or	$⊢ (A ∖ \{−∞\} \subseteq ℝ \lor +∞ \in (A ∖ \{−∞\}) \lor −∞ \in (A ∖ \{−∞\})) \leftrightarrow ((A ∖ \{−∞\} \subseteq ℝ \lor +∞ \in (A ∖ \{−∞\})) \lor −∞ \in (A ∖ \{−∞\}))$
5		neldifsn	$⊢ \neg −∞ \in (A ∖ \{−∞\})$
6	5	biorfri	$⊢ (A ∖ \{−∞\} \subseteq ℝ \lor +∞ \in (A ∖ \{−∞\})) \leftrightarrow ((A ∖ \{−∞\} \subseteq ℝ \lor +∞ \in (A ∖ \{−∞\})) \lor −∞ \in (A ∖ \{−∞\}))$
7	4 6	bitr4i	$⊢ (A ∖ \{−∞\} \subseteq ℝ \lor +∞ \in (A ∖ \{−∞\}) \lor −∞ \in (A ∖ \{−∞\})) \leftrightarrow (A ∖ \{−∞\} \subseteq ℝ \lor +∞ \in (A ∖ \{−∞\}))$
8	3 7	sylib	$⊢ A ∖ \{−∞\} \subseteq ℝ^{*} \to (A ∖ \{−∞\} \subseteq ℝ \lor +∞ \in (A ∖ \{−∞\}))$
9		xrsupsslem	$⊢ (A ∖ \{−∞\} \subseteq ℝ^{} \land (A ∖ \{−∞\} \subseteq ℝ \lor +∞ \in (A ∖ \{−∞\}))) \to \exists x \in ℝ^{} (\forall y \in (A ∖ \{−∞\}) \neg x < y \land \forall y \in ℝ^{*} (y < x \to \exists z \in (A ∖ \{−∞\}) y < z))$
10	2 8 9	syl2anc2	$⊢ A \subseteq ℝ^{} \to \exists x \in ℝ^{} (\forall y \in (A ∖ \{−∞\}) \neg x < y \land \forall y \in ℝ^{*} (y < x \to \exists z \in (A ∖ \{−∞\}) y < z))$
11		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))$
12		snssi	$⊢ −∞ \in A \to \{−∞\} \subseteq A$
13		undif	$⊢ \{−∞\} \subseteq A \leftrightarrow \{−∞\} \cup (A ∖ \{−∞\}) = A$
14		uncom	$⊢ \{−∞\} \cup (A ∖ \{−∞\}) = (A ∖ \{−∞\}) \cup \{−∞\}$
15	14	eqeq1i	$⊢ \{−∞\} \cup (A ∖ \{−∞\}) = A \leftrightarrow (A ∖ \{−∞\}) \cup \{−∞\} = A$
16	13 15	bitri	$⊢ \{−∞\} \subseteq A \leftrightarrow (A ∖ \{−∞\}) \cup \{−∞\} = A$
17		raleq	$⊢ (A ∖ \{−∞\}) \cup \{−∞\} = A \to (\forall y \in ((A ∖ \{−∞\}) \cup \{−∞\}) \neg x < y \leftrightarrow \forall y \in A \neg x < y)$
18		rexeq	$⊢ (A ∖ \{−∞\}) \cup \{−∞\} = A \to (\exists z \in ((A ∖ \{−∞\}) \cup \{−∞\}) y < z \leftrightarrow \exists z \in A y < z)$
19	18	imbi2d	$⊢ (A ∖ \{−∞\}) \cup \{−∞\} = A \to ((y < x \to \exists z \in ((A ∖ \{−∞\}) \cup \{−∞\}) y < z) \leftrightarrow (y < x \to \exists z \in A y < z))$
20	19	ralbidv	$⊢ (A ∖ \{−∞\}) \cup \{−∞\} = A \to (\forall y \in ℝ^{} (y < x \to \exists z \in ((A ∖ \{−∞\}) \cup \{−∞\}) y < z) \leftrightarrow \forall y \in ℝ^{} (y < x \to \exists z \in A y < z))$
21	17 20	anbi12d	$⊢ (A ∖ \{−∞\}) \cup \{−∞\} = A \to ((\forall y \in ((A ∖ \{−∞\}) \cup \{−∞\}) \neg x < y \land \forall y \in ℝ^{} (y < x \to \exists z \in ((A ∖ \{−∞\}) \cup \{−∞\}) y < z)) \leftrightarrow (\forall y \in A \neg x < y \land \forall y \in ℝ^{} (y < x \to \exists z \in A y < z)))$
22	16 21	sylbi	$⊢ \{−∞\} \subseteq A \to ((\forall y \in ((A ∖ \{−∞\}) \cup \{−∞\}) \neg x < y \land \forall y \in ℝ^{} (y < x \to \exists z \in ((A ∖ \{−∞\}) \cup \{−∞\}) y < z)) \leftrightarrow (\forall y \in A \neg x < y \land \forall y \in ℝ^{} (y < x \to \exists z \in A y < z)))$
23	12 22	syl	$⊢ −∞ \in A \to ((\forall y \in ((A ∖ \{−∞\}) \cup \{−∞\}) \neg x < y \land \forall y \in ℝ^{} (y < x \to \exists z \in ((A ∖ \{−∞\}) \cup \{−∞\}) y < z)) \leftrightarrow (\forall y \in A \neg x < y \land \forall y \in ℝ^{} (y < x \to \exists z \in A y < z)))$
24	23	rexbidv	$⊢ −∞ \in A \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)) \leftrightarrow \exists x \in ℝ^{} (\forall y \in A \neg x < y \land \forall y \in ℝ^{} (y < x \to \exists z \in A y < z)))$
25	11 24	imbitrid	$⊢ −∞ \in A \to (\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 \neg x < y \land \forall y \in ℝ^{} (y < x \to \exists z \in A y < z)))$
26	10 25	mpan9	$⊢ (A \subseteq ℝ^{} \land −∞ \in A) \to \exists x \in ℝ^{} (\forall y \in A \neg x < y \land \forall y \in ℝ^{*} (y < x \to \exists z \in A y < z))$
27		ssxr	$⊢ A \subseteq ℝ^{*} \to (A \subseteq ℝ \lor +∞ \in A \lor −∞ \in A)$
28		df-3or	$⊢ (A \subseteq ℝ \lor +∞ \in A \lor −∞ \in A) \leftrightarrow ((A \subseteq ℝ \lor +∞ \in A) \lor −∞ \in A)$
29	27 28	sylib	$⊢ A \subseteq ℝ^{*} \to ((A \subseteq ℝ \lor +∞ \in A) \lor −∞ \in A)$
30	1 26 29	mpjaodan	$⊢ A \subseteq ℝ^{} \to \exists x \in ℝ^{} (\forall y \in A \neg x < y \land \forall y \in ℝ^{*} (y < x \to \exists z \in A y < z))$

Metamath Proof Explorer

Theorem xrsupss

Proof