This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem infmremnf

Description: The infimum of the reals is minus infinity. (Contributed by AV, 5-Sep-2020)

		Ref	Expression
	Assertion	infmremnf	$⊢ inf (ℝ ℝ^{*} <) = −∞$

Proof

Step	Hyp	Ref	Expression
1		reltxrnmnf	$⊢ \forall x \in ℝ^{*} (−∞ < x \to \exists z \in ℝ z < x)$
2		xrltso	$⊢ < Or ℝ^{*}$
3	2	a1i	$⊢ \forall x \in ℝ^{} (−∞ < x \to \exists z \in ℝ z < x) \to < Or ℝ^{}$
4		mnfxr	$⊢ −∞ \in ℝ^{*}$
5	4	a1i	$⊢ \forall x \in ℝ^{} (−∞ < x \to \exists z \in ℝ z < x) \to −∞ \in ℝ^{}$
6		rexr	$⊢ y \in ℝ \to y \in ℝ^{*}$
7		nltmnf	$⊢ y \in ℝ^{*} \to \neg y < −∞$
8	6 7	syl	$⊢ y \in ℝ \to \neg y < −∞$
9	8	adantl	$⊢ (\forall x \in ℝ^{*} (−∞ < x \to \exists z \in ℝ z < x) \land y \in ℝ) \to \neg y < −∞$
10		breq2	$⊢ x = y \to (−∞ < x \leftrightarrow −∞ < y)$
11		breq2	$⊢ x = y \to (z < x \leftrightarrow z < y)$
12	11	rexbidv	$⊢ x = y \to (\exists z \in ℝ z < x \leftrightarrow \exists z \in ℝ z < y)$
13	10 12	imbi12d	$⊢ x = y \to ((−∞ < x \to \exists z \in ℝ z < x) \leftrightarrow (−∞ < y \to \exists z \in ℝ z < y))$
14	13	rspcv	$⊢ y \in ℝ^{} \to (\forall x \in ℝ^{} (−∞ < x \to \exists z \in ℝ z < x) \to (−∞ < y \to \exists z \in ℝ z < y))$
15	14	com23	$⊢ y \in ℝ^{} \to (−∞ < y \to (\forall x \in ℝ^{} (−∞ < x \to \exists z \in ℝ z < x) \to \exists z \in ℝ z < y))$
16	15	imp	$⊢ (y \in ℝ^{} \land −∞ < y) \to (\forall x \in ℝ^{} (−∞ < x \to \exists z \in ℝ z < x) \to \exists z \in ℝ z < y)$
17	16	impcom	$⊢ (\forall x \in ℝ^{} (−∞ < x \to \exists z \in ℝ z < x) \land (y \in ℝ^{} \land −∞ < y)) \to \exists z \in ℝ z < y$
18	3 5 9 17	eqinfd	$⊢ \forall x \in ℝ^{} (−∞ < x \to \exists z \in ℝ z < x) \to inf (ℝ ℝ^{} <) = −∞$
19	1 18	ax-mp	$⊢ inf (ℝ ℝ^{*} <) = −∞$