infxrre

Description: The real and extended real infima match when the real infimum exists. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 5-Sep-2020)

		Ref	Expression
	Assertion	infxrre	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to inf (A ℝ^{*} <) = inf (A ℝ <)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to A \subseteq ℝ$
2		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
3	1 2	sstrdi	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to A \subseteq ℝ^{*}$
4		infxrcl	$⊢ A \subseteq ℝ^{} \to inf (A ℝ^{} <) \in ℝ^{*}$
5	3 4	syl	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to inf (A ℝ^{} <) \in ℝ^{}$
6		infrecl	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to inf (A ℝ <) \in ℝ$
7	6	rexrd	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to inf (A ℝ <) \in ℝ^{*}$
8	5	xrleidd	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to inf (A ℝ^{} <) \leq inf (A ℝ^{} <)$
9		infxrgelb	$⊢ (A \subseteq ℝ^{} \land inf (A ℝ^{} <) \in ℝ^{}) \to (inf (A ℝ^{} <) \leq inf (A ℝ^{} <) \leftrightarrow \forall x \in A inf (A ℝ^{} <) \leq x)$
10	3 5 9	syl2anc	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to (inf (A ℝ^{} <) \leq inf (A ℝ^{} <) \leftrightarrow \forall x \in A inf (A ℝ^{*} <) \leq x)$
11		simp2	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to A \neq \emptyset$
12		n0	$⊢ A \neq \emptyset \leftrightarrow \exists z z \in A$
13	11 12	sylib	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to \exists z z \in A$
14	5	adantr	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \land z \in A) \to inf (A ℝ^{} <) \in ℝ^{}$
15	1	sselda	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \land z \in A) \to z \in ℝ$
16		mnfxr	$⊢ −∞ \in ℝ^{*}$
17	16	a1i	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to −∞ \in ℝ^{*}$
18	6	mnfltd	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to −∞ < inf (A ℝ <)$
19	6	leidd	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to inf (A ℝ <) \leq inf (A ℝ <)$
20		infregelb	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \land inf (A ℝ <) \in ℝ) \to (inf (A ℝ <) \leq inf (A ℝ <) \leftrightarrow \forall x \in A inf (A ℝ <) \leq x)$
21	6 20	mpdan	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to (inf (A ℝ <) \leq inf (A ℝ <) \leftrightarrow \forall x \in A inf (A ℝ <) \leq x)$
22		infxrgelb	$⊢ (A \subseteq ℝ^{} \land inf (A ℝ <) \in ℝ^{}) \to (inf (A ℝ <) \leq inf (A ℝ^{*} <) \leftrightarrow \forall x \in A inf (A ℝ <) \leq x)$
23	3 7 22	syl2anc	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to (inf (A ℝ <) \leq inf (A ℝ^{*} <) \leftrightarrow \forall x \in A inf (A ℝ <) \leq x)$
24	21 23	bitr4d	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to (inf (A ℝ <) \leq inf (A ℝ <) \leftrightarrow inf (A ℝ <) \leq inf (A ℝ^{*} <))$
25	19 24	mpbid	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to inf (A ℝ <) \leq inf (A ℝ^{*} <)$
26	17 7 5 18 25	xrltletrd	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to −∞ < inf (A ℝ^{*} <)$
27	26	adantr	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \land z \in A) \to −∞ < inf (A ℝ^{*} <)$
28		infxrlb	$⊢ (A \subseteq ℝ^{} \land z \in A) \to inf (A ℝ^{} <) \leq z$
29	3 28	sylan	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \land z \in A) \to inf (A ℝ^{*} <) \leq z$
30		xrre	$⊢ ((inf (A ℝ^{} <) \in ℝ^{} \land z \in ℝ) \land (−∞ < inf (A ℝ^{} <) \land inf (A ℝ^{} <) \leq z)) \to inf (A ℝ^{*} <) \in ℝ$
31	14 15 27 29 30	syl22anc	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \land z \in A) \to inf (A ℝ^{*} <) \in ℝ$
32	13 31	exlimddv	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to inf (A ℝ^{*} <) \in ℝ$
33		infregelb	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \land inf (A ℝ^{} <) \in ℝ) \to (inf (A ℝ^{} <) \leq inf (A ℝ <) \leftrightarrow \forall x \in A inf (A ℝ^{*} <) \leq x)$
34	32 33	mpdan	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to (inf (A ℝ^{} <) \leq inf (A ℝ <) \leftrightarrow \forall x \in A inf (A ℝ^{} <) \leq x)$
35	10 34	bitr4d	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to (inf (A ℝ^{} <) \leq inf (A ℝ^{} <) \leftrightarrow inf (A ℝ^{*} <) \leq inf (A ℝ <))$
36	8 35	mpbid	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to inf (A ℝ^{*} <) \leq inf (A ℝ <)$
37	5 7 36 25	xrletrid	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to inf (A ℝ^{*} <) = inf (A ℝ <)$

Metamath Proof Explorer

Theorem infxrre

Proof