xrinfmss

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

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

Proof

Step	Hyp	Ref	Expression
1		xrinfmsslem	$⊢ (A \subseteq ℝ^{} \land (A \subseteq ℝ \lor −∞ \in A)) \to \exists x \in ℝ^{} (\forall y \in A \neg y < x \land \forall y \in ℝ^{*} (x < y \to \exists z \in A z < y))$
2		ssdifss	$⊢ A \subseteq ℝ^{} \to A ∖ \{+∞\} \subseteq ℝ^{}$
3		ssxr	$⊢ A ∖ \{+∞\} \subseteq ℝ^{*} \to (A ∖ \{+∞\} \subseteq ℝ \lor +∞ \in (A ∖ \{+∞\}) \lor −∞ \in (A ∖ \{+∞\}))$
4		3orass	$⊢ (A ∖ \{+∞\} \subseteq ℝ \lor +∞ \in (A ∖ \{+∞\}) \lor −∞ \in (A ∖ \{+∞\})) \leftrightarrow (A ∖ \{+∞\} \subseteq ℝ \lor (+∞ \in (A ∖ \{+∞\}) \lor −∞ \in (A ∖ \{+∞\})))$
5		pnfex	$⊢ +∞ \in V$
6	5	snid	$⊢ +∞ \in \{+∞\}$
7		elndif	$⊢ +∞ \in \{+∞\} \to \neg +∞ \in (A ∖ \{+∞\})$
8		biorf	$⊢ \neg +∞ \in (A ∖ \{+∞\}) \to (−∞ \in (A ∖ \{+∞\}) \leftrightarrow (+∞ \in (A ∖ \{+∞\}) \lor −∞ \in (A ∖ \{+∞\})))$
9	6 7 8	mp2b	$⊢ −∞ \in (A ∖ \{+∞\}) \leftrightarrow (+∞ \in (A ∖ \{+∞\}) \lor −∞ \in (A ∖ \{+∞\}))$
10	9	orbi2i	$⊢ (A ∖ \{+∞\} \subseteq ℝ \lor −∞ \in (A ∖ \{+∞\})) \leftrightarrow (A ∖ \{+∞\} \subseteq ℝ \lor (+∞ \in (A ∖ \{+∞\}) \lor −∞ \in (A ∖ \{+∞\})))$
11	4 10	bitr4i	$⊢ (A ∖ \{+∞\} \subseteq ℝ \lor +∞ \in (A ∖ \{+∞\}) \lor −∞ \in (A ∖ \{+∞\})) \leftrightarrow (A ∖ \{+∞\} \subseteq ℝ \lor −∞ \in (A ∖ \{+∞\}))$
12	3 11	sylib	$⊢ A ∖ \{+∞\} \subseteq ℝ^{*} \to (A ∖ \{+∞\} \subseteq ℝ \lor −∞ \in (A ∖ \{+∞\}))$
13		xrinfmsslem	$⊢ (A ∖ \{+∞\} \subseteq ℝ^{} \land (A ∖ \{+∞\} \subseteq ℝ \lor −∞ \in (A ∖ \{+∞\}))) \to \exists x \in ℝ^{} (\forall y \in (A ∖ \{+∞\}) \neg y < x \land \forall y \in ℝ^{*} (x < y \to \exists z \in (A ∖ \{+∞\}) z < y))$
14	2 12 13	syl2anc2	$⊢ A \subseteq ℝ^{} \to \exists x \in ℝ^{} (\forall y \in (A ∖ \{+∞\}) \neg y < x \land \forall y \in ℝ^{*} (x < y \to \exists z \in (A ∖ \{+∞\}) z < y))$
15		xrinfmexpnf	$⊢ \exists x \in ℝ^{} (\forall y \in (A ∖ \{+∞\}) \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in (A ∖ \{+∞\}) z < y)) \to \exists x \in ℝ^{} (\forall y \in ((A ∖ \{+∞\}) \cup \{+∞\}) \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in ((A ∖ \{+∞\}) \cup \{+∞\}) z < y))$
16	5	snss	$⊢ +∞ \in A \leftrightarrow \{+∞\} \subseteq A$
17		undif	$⊢ \{+∞\} \subseteq A \leftrightarrow \{+∞\} \cup (A ∖ \{+∞\}) = A$
18		uncom	$⊢ \{+∞\} \cup (A ∖ \{+∞\}) = (A ∖ \{+∞\}) \cup \{+∞\}$
19	18	eqeq1i	$⊢ \{+∞\} \cup (A ∖ \{+∞\}) = A \leftrightarrow (A ∖ \{+∞\}) \cup \{+∞\} = A$
20	17 19	bitri	$⊢ \{+∞\} \subseteq A \leftrightarrow (A ∖ \{+∞\}) \cup \{+∞\} = A$
21	16 20	bitri	$⊢ +∞ \in A \leftrightarrow (A ∖ \{+∞\}) \cup \{+∞\} = A$
22		raleq	$⊢ (A ∖ \{+∞\}) \cup \{+∞\} = A \to (\forall y \in ((A ∖ \{+∞\}) \cup \{+∞\}) \neg y < x \leftrightarrow \forall y \in A \neg y < x)$
23		rexeq	$⊢ (A ∖ \{+∞\}) \cup \{+∞\} = A \to (\exists z \in ((A ∖ \{+∞\}) \cup \{+∞\}) z < y \leftrightarrow \exists z \in A z < y)$
24	23	imbi2d	$⊢ (A ∖ \{+∞\}) \cup \{+∞\} = A \to ((x < y \to \exists z \in ((A ∖ \{+∞\}) \cup \{+∞\}) z < y) \leftrightarrow (x < y \to \exists z \in A z < y))$
25	24	ralbidv	$⊢ (A ∖ \{+∞\}) \cup \{+∞\} = A \to (\forall y \in ℝ^{} (x < y \to \exists z \in ((A ∖ \{+∞\}) \cup \{+∞\}) z < y) \leftrightarrow \forall y \in ℝ^{} (x < y \to \exists z \in A z < y))$
26	22 25	anbi12d	$⊢ (A ∖ \{+∞\}) \cup \{+∞\} = A \to ((\forall y \in ((A ∖ \{+∞\}) \cup \{+∞\}) \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in ((A ∖ \{+∞\}) \cup \{+∞\}) z < y)) \leftrightarrow (\forall y \in A \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in A z < y)))$
27	21 26	sylbi	$⊢ +∞ \in A \to ((\forall y \in ((A ∖ \{+∞\}) \cup \{+∞\}) \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in ((A ∖ \{+∞\}) \cup \{+∞\}) z < y)) \leftrightarrow (\forall y \in A \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in A z < y)))$
28	27	rexbidv	$⊢ +∞ \in A \to (\exists x \in ℝ^{} (\forall y \in ((A ∖ \{+∞\}) \cup \{+∞\}) \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in ((A ∖ \{+∞\}) \cup \{+∞\}) z < y)) \leftrightarrow \exists x \in ℝ^{} (\forall y \in A \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in A z < y)))$
29	15 28	syl5ib	$⊢ +∞ \in A \to (\exists x \in ℝ^{} (\forall y \in (A ∖ \{+∞\}) \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in (A ∖ \{+∞\}) z < y)) \to \exists x \in ℝ^{} (\forall y \in A \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in A z < y)))$
30	14 29	mpan9	$⊢ (A \subseteq ℝ^{} \land +∞ \in A) \to \exists x \in ℝ^{} (\forall y \in A \neg y < x \land \forall y \in ℝ^{*} (x < y \to \exists z \in A z < y))$
31		ssxr	$⊢ A \subseteq ℝ^{*} \to (A \subseteq ℝ \lor +∞ \in A \lor −∞ \in A)$
32		df-3or	$⊢ (A \subseteq ℝ \lor +∞ \in A \lor −∞ \in A) \leftrightarrow ((A \subseteq ℝ \lor +∞ \in A) \lor −∞ \in A)$
33		or32	$⊢ ((A \subseteq ℝ \lor +∞ \in A) \lor −∞ \in A) \leftrightarrow ((A \subseteq ℝ \lor −∞ \in A) \lor +∞ \in A)$
34	32 33	bitri	$⊢ (A \subseteq ℝ \lor +∞ \in A \lor −∞ \in A) \leftrightarrow ((A \subseteq ℝ \lor −∞ \in A) \lor +∞ \in A)$
35	31 34	sylib	$⊢ A \subseteq ℝ^{*} \to ((A \subseteq ℝ \lor −∞ \in A) \lor +∞ \in A)$
36	1 30 35	mpjaodan	$⊢ A \subseteq ℝ^{} \to \exists x \in ℝ^{} (\forall y \in A \neg y < x \land \forall y \in ℝ^{*} (x < y \to \exists z \in A z < y))$

Metamath Proof Explorer

Theorem xrinfmss

Proof