Metamath Proof Explorer

Theorem infxrbnd2

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

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

Proof

Step	Hyp	Ref	Expression
1		ralnex	$⊢ \forall x \in ℝ \neg \forall y \in A x \leq y \leftrightarrow \neg \exists x \in ℝ \forall y \in A x \leq y$
2		ssel2	$⊢ (A \subseteq ℝ^{} \land y \in A) \to y \in ℝ^{}$
3		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
4		simpl	$⊢ (y \in ℝ^{} \land x \in ℝ^{}) \to y \in ℝ^{*}$
5		simpr	$⊢ (y \in ℝ^{} \land x \in ℝ^{}) \to x \in ℝ^{*}$
6	4 5	xrltnled	$⊢ (y \in ℝ^{} \land x \in ℝ^{}) \to (y < x \leftrightarrow \neg x \leq y)$
7	2 3 6	syl2an	$⊢ ((A \subseteq ℝ^{*} \land y \in A) \land x \in ℝ) \to (y < x \leftrightarrow \neg x \leq y)$
8	7	an32s	$⊢ ((A \subseteq ℝ^{*} \land x \in ℝ) \land y \in A) \to (y < x \leftrightarrow \neg x \leq y)$
9	8	rexbidva	$⊢ (A \subseteq ℝ^{*} \land x \in ℝ) \to (\exists y \in A y < x \leftrightarrow \exists y \in A \neg x \leq y)$
10		rexnal	$⊢ \exists y \in A \neg x \leq y \leftrightarrow \neg \forall y \in A x \leq y$
11	9 10	bitr2di	$⊢ (A \subseteq ℝ^{*} \land x \in ℝ) \to (\neg \forall y \in A x \leq y \leftrightarrow \exists y \in A y < x)$
12	11	ralbidva	$⊢ A \subseteq ℝ^{*} \to (\forall x \in ℝ \neg \forall y \in A x \leq y \leftrightarrow \forall x \in ℝ \exists y \in A y < x)$
13	1 12	bitr3id	$⊢ A \subseteq ℝ^{*} \to (\neg \exists x \in ℝ \forall y \in A x \leq y \leftrightarrow \forall x \in ℝ \exists y \in A y < x)$
14		infxrunb2	$⊢ A \subseteq ℝ^{} \to (\forall x \in ℝ \exists y \in A y < x \leftrightarrow sup (A ℝ^{} <) = −∞)$
15		infxrcl	$⊢ A \subseteq ℝ^{} \to sup (A ℝ^{} <) \in ℝ^{*}$
16		ngtmnft	$⊢ sup (A ℝ^{} <) \in ℝ^{} \to (sup (A ℝ^{} <) = −∞ \leftrightarrow \neg −∞ < sup (A ℝ^{} <))$
17	15 16	syl	$⊢ A \subseteq ℝ^{} \to (sup (A ℝ^{} <) = −∞ \leftrightarrow \neg −∞ < sup (A ℝ^{*} <))$
18	13 14 17	3bitrd	$⊢ A \subseteq ℝ^{} \to (\neg \exists x \in ℝ \forall y \in A x \leq y \leftrightarrow \neg −∞ < sup (A ℝ^{} <))$
19	18	con4bid	$⊢ A \subseteq ℝ^{} \to (\exists x \in ℝ \forall y \in A x \leq y \leftrightarrow −∞ < sup (A ℝ^{} <))$