limsup0

Description: The superior limit of the empty set. (Contributed by Glauco Siliprandi, 23-Oct-2021)

		Ref	Expression
	Assertion	limsup0	$⊢ lim sup (\emptyset) = −∞$

Proof

Step	Hyp	Ref	Expression
1		0ex	$⊢ \emptyset \in V$
2		eqid	$⊢ (x \in ℝ ⟼ sup (\emptyset [[x, +∞)] \cap ℝ^{} ℝ^{} <)) = (x \in ℝ ⟼ sup (\emptyset [[x, +∞)] \cap ℝ^{} ℝ^{} <))$
3	2	limsupval	$⊢ \emptyset \in V \to lim sup (\emptyset) = sup (ran (x \in ℝ ⟼ sup (\emptyset [[x, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
4	1 3	ax-mp	$⊢ lim sup (\emptyset) = sup (ran (x \in ℝ ⟼ sup (\emptyset [[x, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
5		0ima	$⊢ \emptyset [[x, +∞)] = \emptyset$
6	5	ineq1i	$⊢ \emptyset [[x, +∞)] \cap ℝ^{} = \emptyset \cap ℝ^{}$
7		0in	$⊢ \emptyset \cap ℝ^{*} = \emptyset$
8	6 7	eqtri	$⊢ \emptyset [[x, +∞)] \cap ℝ^{*} = \emptyset$
9	8	supeq1i	$⊢ sup (\emptyset [[x, +∞)] \cap ℝ^{} ℝ^{} <) = sup (\emptyset ℝ^{*} <)$
10		xrsup0	$⊢ sup (\emptyset ℝ^{*} <) = −∞$
11	9 10	eqtri	$⊢ sup (\emptyset [[x, +∞)] \cap ℝ^{} ℝ^{} <) = −∞$
12	11	mpteq2i	$⊢ (x \in ℝ ⟼ sup (\emptyset [[x, +∞)] \cap ℝ^{} ℝ^{} <)) = (x \in ℝ ⟼ −∞)$
13		ren0	$⊢ ℝ \neq \emptyset$
14	13	a1i	$⊢ ⊤ \to ℝ \neq \emptyset$
15	12 14	rnmptc	$⊢ ⊤ \to ran (x \in ℝ ⟼ sup (\emptyset [[x, +∞)] \cap ℝ^{} ℝ^{} <)) = \{−∞\}$
16	15	mptru	$⊢ ran (x \in ℝ ⟼ sup (\emptyset [[x, +∞)] \cap ℝ^{} ℝ^{} <)) = \{−∞\}$
17	16	infeq1i	$⊢ sup (ran (x \in ℝ ⟼ sup (\emptyset [[x, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) = sup (\{−∞\} ℝ^{} <)$
18		xrltso	$⊢ < Or ℝ^{*}$
19		mnfxr	$⊢ −∞ \in ℝ^{*}$
20		infsn	$⊢ (< Or ℝ^{} \land −∞ \in ℝ^{}) \to sup (\{−∞\} ℝ^{*} <) = −∞$
21	18 19 20	mp2an	$⊢ sup (\{−∞\} ℝ^{*} <) = −∞$
22	4 17 21	3eqtri	$⊢ lim sup (\emptyset) = −∞$

Metamath Proof Explorer

Theorem limsup0

Proof