infxrunb2

Description: The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021)

		Ref	Expression
	Assertion	infxrunb2	$⊢ A \subseteq ℝ^{} \to (\forall x \in ℝ \exists y \in A y < x \leftrightarrow inf (A ℝ^{} <) = −∞)$

Proof

Step	Hyp	Ref	Expression
1		nfv	$⊢ Ⅎ x A \subseteq ℝ^{*}$
2		nfra1	$⊢ Ⅎ x \forall x \in ℝ \exists y \in A y < x$
3	1 2	nfan	$⊢ Ⅎ x (A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A y < x)$
4		nfv	$⊢ Ⅎ y A \subseteq ℝ^{*}$
5		nfcv	$⊢ \underline{Ⅎ} y ℝ$
6		nfre1	$⊢ Ⅎ y \exists y \in A y < x$
7	5 6	nfralw	$⊢ Ⅎ y \forall x \in ℝ \exists y \in A y < x$
8	4 7	nfan	$⊢ Ⅎ y (A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A y < x)$
9		simpl	$⊢ (A \subseteq ℝ^{} \land \forall x \in ℝ \exists y \in A y < x) \to A \subseteq ℝ^{}$
10		mnfxr	$⊢ −∞ \in ℝ^{*}$
11	10	a1i	$⊢ (A \subseteq ℝ^{} \land \forall x \in ℝ \exists y \in A y < x) \to −∞ \in ℝ^{}$
12		ssel2	$⊢ (A \subseteq ℝ^{} \land x \in A) \to x \in ℝ^{}$
13		nltmnf	$⊢ x \in ℝ^{*} \to \neg x < −∞$
14	12 13	syl	$⊢ (A \subseteq ℝ^{*} \land x \in A) \to \neg x < −∞$
15	14	ralrimiva	$⊢ A \subseteq ℝ^{*} \to \forall x \in A \neg x < −∞$
16	15	adantr	$⊢ (A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A y < x) \to \forall x \in A \neg x < −∞$
17		ralimralim	$⊢ \forall x \in ℝ \exists y \in A y < x \to \forall x \in ℝ (−∞ < x \to \exists y \in A y < x)$
18	17	adantl	$⊢ (A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A y < x) \to \forall x \in ℝ (−∞ < x \to \exists y \in A y < x)$
19	3 8 9 11 16 18	infxr	$⊢ (A \subseteq ℝ^{} \land \forall x \in ℝ \exists y \in A y < x) \to inf (A ℝ^{} <) = −∞$
20	19	ex	$⊢ A \subseteq ℝ^{} \to (\forall x \in ℝ \exists y \in A y < x \to inf (A ℝ^{} <) = −∞)$
21		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
22	21	adantl	$⊢ ((A \subseteq ℝ^{} \land inf (A ℝ^{} <) = −∞) \land x \in ℝ) \to x \in ℝ^{*}$
23		simpl	$⊢ (inf (A ℝ^{} <) = −∞ \land x \in ℝ) \to inf (A ℝ^{} <) = −∞$
24		mnflt	$⊢ x \in ℝ \to −∞ < x$
25	24	adantl	$⊢ (inf (A ℝ^{*} <) = −∞ \land x \in ℝ) \to −∞ < x$
26	23 25	eqbrtrd	$⊢ (inf (A ℝ^{} <) = −∞ \land x \in ℝ) \to inf (A ℝ^{} <) < x$
27	26	adantll	$⊢ ((A \subseteq ℝ^{} \land inf (A ℝ^{} <) = −∞) \land x \in ℝ) \to inf (A ℝ^{*} <) < x$
28		xrltso	$⊢ < Or ℝ^{*}$
29	28	a1i	$⊢ ((A \subseteq ℝ^{} \land inf (A ℝ^{} <) = −∞) \land x \in ℝ) \to < Or ℝ^{*}$
30		xrinfmss	$⊢ A \subseteq ℝ^{} \to \exists z \in ℝ^{} (\forall w \in A \neg w < z \land \forall w \in ℝ^{*} (z < w \to \exists y \in A y < w))$
31	30	ad2antrr	$⊢ ((A \subseteq ℝ^{} \land inf (A ℝ^{} <) = −∞) \land x \in ℝ) \to \exists z \in ℝ^{} (\forall w \in A \neg w < z \land \forall w \in ℝ^{} (z < w \to \exists y \in A y < w))$
32	29 31	infglb	$⊢ ((A \subseteq ℝ^{} \land inf (A ℝ^{} <) = −∞) \land x \in ℝ) \to ((x \in ℝ^{} \land inf (A ℝ^{} <) < x) \to \exists y \in A y < x)$
33	22 27 32	mp2and	$⊢ ((A \subseteq ℝ^{} \land inf (A ℝ^{} <) = −∞) \land x \in ℝ) \to \exists y \in A y < x$
34	33	ralrimiva	$⊢ (A \subseteq ℝ^{} \land inf (A ℝ^{} <) = −∞) \to \forall x \in ℝ \exists y \in A y < x$
35	34	ex	$⊢ A \subseteq ℝ^{} \to (inf (A ℝ^{} <) = −∞ \to \forall x \in ℝ \exists y \in A y < x)$
36	20 35	impbid	$⊢ A \subseteq ℝ^{} \to (\forall x \in ℝ \exists y \in A y < x \leftrightarrow inf (A ℝ^{} <) = −∞)$

Metamath Proof Explorer

Theorem infxrunb2

Proof