infxrpnf

Description: Adding plus infinity to a set does not affect its infimum. (Contributed by Glauco Siliprandi, 2-Jan-2022)

		Ref	Expression
	Assertion	infxrpnf	$⊢ A \subseteq ℝ^{} \to inf (A \cup \{+∞\} ℝ^{} <) = inf (A ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ A \subseteq ℝ^{} \to A \subseteq ℝ^{}$
2		pnfxr	$⊢ +∞ \in ℝ^{*}$
3		snssi	$⊢ +∞ \in ℝ^{} \to \{+∞\} \subseteq ℝ^{}$
4	2 3	ax-mp	$⊢ \{+∞\} \subseteq ℝ^{*}$
5	4	a1i	$⊢ A \subseteq ℝ^{} \to \{+∞\} \subseteq ℝ^{}$
6	1 5	unssd	$⊢ A \subseteq ℝ^{} \to A \cup \{+∞\} \subseteq ℝ^{}$
7	6	infxrcld	$⊢ A \subseteq ℝ^{} \to inf (A \cup \{+∞\} ℝ^{} <) \in ℝ^{*}$
8		infxrcl	$⊢ A \subseteq ℝ^{} \to inf (A ℝ^{} <) \in ℝ^{*}$
9		ssun1	$⊢ A \subseteq A \cup \{+∞\}$
10	9	a1i	$⊢ A \subseteq ℝ^{*} \to A \subseteq A \cup \{+∞\}$
11		infxrss	$⊢ (A \subseteq A \cup \{+∞\} \land A \cup \{+∞\} \subseteq ℝ^{}) \to inf (A \cup \{+∞\} ℝ^{} <) \leq inf (A ℝ^{*} <)$
12	10 6 11	syl2anc	$⊢ A \subseteq ℝ^{} \to inf (A \cup \{+∞\} ℝ^{} <) \leq inf (A ℝ^{*} <)$
13		infeq1	$⊢ A = \emptyset \to inf (A ℝ^{} <) = inf (\emptyset ℝ^{} <)$
14		xrinf0	$⊢ inf (\emptyset ℝ^{*} <) = +∞$
15	14 2	eqeltri	$⊢ inf (\emptyset ℝ^{} <) \in ℝ^{}$
16	15	a1i	$⊢ A = \emptyset \to inf (\emptyset ℝ^{} <) \in ℝ^{}$
17	13 16	eqeltrd	$⊢ A = \emptyset \to inf (A ℝ^{} <) \in ℝ^{}$
18		xrltso	$⊢ < Or ℝ^{*}$
19		infsn	$⊢ (< Or ℝ^{} \land +∞ \in ℝ^{}) \to inf (\{+∞\} ℝ^{*} <) = +∞$
20	18 2 19	mp2an	$⊢ inf (\{+∞\} ℝ^{*} <) = +∞$
21	20	eqcomi	$⊢ +∞ = inf (\{+∞\} ℝ^{*} <)$
22	21	a1i	$⊢ A = \emptyset \to +∞ = inf (\{+∞\} ℝ^{*} <)$
23	13 14	eqtrdi	$⊢ A = \emptyset \to inf (A ℝ^{*} <) = +∞$
24		uneq1	$⊢ A = \emptyset \to A \cup \{+∞\} = \emptyset \cup \{+∞\}$
25		0un	$⊢ \emptyset \cup \{+∞\} = \{+∞\}$
26	25	a1i	$⊢ A = \emptyset \to \emptyset \cup \{+∞\} = \{+∞\}$
27	24 26	eqtrd	$⊢ A = \emptyset \to A \cup \{+∞\} = \{+∞\}$
28	27	infeq1d	$⊢ A = \emptyset \to inf (A \cup \{+∞\} ℝ^{} <) = inf (\{+∞\} ℝ^{} <)$
29	22 23 28	3eqtr4d	$⊢ A = \emptyset \to inf (A ℝ^{} <) = inf (A \cup \{+∞\} ℝ^{} <)$
30	17 29	xreqled	$⊢ A = \emptyset \to inf (A ℝ^{} <) \leq inf (A \cup \{+∞\} ℝ^{} <)$
31	30	adantl	$⊢ (A \subseteq ℝ^{} \land A = \emptyset) \to inf (A ℝ^{} <) \leq inf (A \cup \{+∞\} ℝ^{*} <)$
32		neqne	$⊢ \neg A = \emptyset \to A \neq \emptyset$
33		nfv	$⊢ Ⅎ x (A \subseteq ℝ^{*} \land A \neq \emptyset)$
34		nfv	$⊢ Ⅎ y (A \subseteq ℝ^{*} \land A \neq \emptyset)$
35		simpl	$⊢ (A \subseteq ℝ^{} \land A \neq \emptyset) \to A \subseteq ℝ^{}$
36	35 6	syl	$⊢ (A \subseteq ℝ^{} \land A \neq \emptyset) \to A \cup \{+∞\} \subseteq ℝ^{}$
37		simpr	$⊢ (A \subseteq ℝ^{*} \land x \in A) \to x \in A$
38		ssel2	$⊢ (A \subseteq ℝ^{} \land x \in A) \to x \in ℝ^{}$
39	38	xrleidd	$⊢ (A \subseteq ℝ^{*} \land x \in A) \to x \leq x$
40		breq1	$⊢ y = x \to (y \leq x \leftrightarrow x \leq x)$
41	40	rspcev	$⊢ (x \in A \land x \leq x) \to \exists y \in A y \leq x$
42	37 39 41	syl2anc	$⊢ (A \subseteq ℝ^{*} \land x \in A) \to \exists y \in A y \leq x$
43	42	ad4ant14	$⊢ (((A \subseteq ℝ^{*} \land A \neq \emptyset) \land x \in (A \cup \{+∞\})) \land x \in A) \to \exists y \in A y \leq x$
44		simpll	$⊢ (((A \subseteq ℝ^{} \land A \neq \emptyset) \land x \in (A \cup \{+∞\})) \land \neg x \in A) \to (A \subseteq ℝ^{} \land A \neq \emptyset)$
45		elunnel1	$⊢ (x \in (A \cup \{+∞\}) \land \neg x \in A) \to x \in \{+∞\}$
46		elsni	$⊢ x \in \{+∞\} \to x = +∞$
47	45 46	syl	$⊢ (x \in (A \cup \{+∞\}) \land \neg x \in A) \to x = +∞$
48	47	adantll	$⊢ (((A \subseteq ℝ^{*} \land A \neq \emptyset) \land x \in (A \cup \{+∞\})) \land \neg x \in A) \to x = +∞$
49		simplr	$⊢ ((A \subseteq ℝ^{*} \land A \neq \emptyset) \land x = +∞) \to A \neq \emptyset$
50		ssel2	$⊢ (A \subseteq ℝ^{} \land y \in A) \to y \in ℝ^{}$
51		pnfge	$⊢ y \in ℝ^{*} \to y \leq +∞$
52	50 51	syl	$⊢ (A \subseteq ℝ^{*} \land y \in A) \to y \leq +∞$
53	52	adantlr	$⊢ ((A \subseteq ℝ^{*} \land x = +∞) \land y \in A) \to y \leq +∞$
54		simplr	$⊢ ((A \subseteq ℝ^{*} \land x = +∞) \land y \in A) \to x = +∞$
55	53 54	breqtrrd	$⊢ ((A \subseteq ℝ^{*} \land x = +∞) \land y \in A) \to y \leq x$
56	55	ralrimiva	$⊢ (A \subseteq ℝ^{*} \land x = +∞) \to \forall y \in A y \leq x$
57	56	adantlr	$⊢ ((A \subseteq ℝ^{*} \land A \neq \emptyset) \land x = +∞) \to \forall y \in A y \leq x$
58		r19.2z	$⊢ (A \neq \emptyset \land \forall y \in A y \leq x) \to \exists y \in A y \leq x$
59	49 57 58	syl2anc	$⊢ ((A \subseteq ℝ^{*} \land A \neq \emptyset) \land x = +∞) \to \exists y \in A y \leq x$
60	44 48 59	syl2anc	$⊢ (((A \subseteq ℝ^{*} \land A \neq \emptyset) \land x \in (A \cup \{+∞\})) \land \neg x \in A) \to \exists y \in A y \leq x$
61	43 60	pm2.61dan	$⊢ ((A \subseteq ℝ^{*} \land A \neq \emptyset) \land x \in (A \cup \{+∞\})) \to \exists y \in A y \leq x$
62	33 34 35 36 61	infleinf2	$⊢ (A \subseteq ℝ^{} \land A \neq \emptyset) \to inf (A ℝ^{} <) \leq inf (A \cup \{+∞\} ℝ^{*} <)$
63	32 62	sylan2	$⊢ (A \subseteq ℝ^{} \land \neg A = \emptyset) \to inf (A ℝ^{} <) \leq inf (A \cup \{+∞\} ℝ^{*} <)$
64	31 63	pm2.61dan	$⊢ A \subseteq ℝ^{} \to inf (A ℝ^{} <) \leq inf (A \cup \{+∞\} ℝ^{*} <)$
65	7 8 12 64	xrletrid	$⊢ A \subseteq ℝ^{} \to inf (A \cup \{+∞\} ℝ^{} <) = inf (A ℝ^{*} <)$

Metamath Proof Explorer

Theorem infxrpnf

Proof