infxr

Description: The infimum of a set of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	infxr.x	$⊢ Ⅎ x φ$
	infxr.y	$⊢ Ⅎ y φ$
	infxr.a	$⊢ φ \to A \subseteq ℝ^{*}$
	infxr.b	$⊢ φ \to B \in ℝ^{*}$
	infxr.n	$⊢ φ \to \forall x \in A \neg x < B$
	infxr.e	$⊢ φ \to \forall x \in ℝ (B < x \to \exists y \in A y < x)$
Assertion	infxr	$⊢ φ \to inf (A ℝ^{*} <) = B$

Proof

Step	Hyp	Ref	Expression
1		infxr.x	$⊢ Ⅎ x φ$
2		infxr.y	$⊢ Ⅎ y φ$
3		infxr.a	$⊢ φ \to A \subseteq ℝ^{*}$
4		infxr.b	$⊢ φ \to B \in ℝ^{*}$
5		infxr.n	$⊢ φ \to \forall x \in A \neg x < B$
6		infxr.e	$⊢ φ \to \forall x \in ℝ (B < x \to \exists y \in A y < x)$
7	6	r19.21bi	$⊢ (φ \land x \in ℝ) \to (B < x \to \exists y \in A y < x)$
8	7	adantlr	$⊢ ((φ \land x \in ℝ^{*}) \land x \in ℝ) \to (B < x \to \exists y \in A y < x)$
9		simplll	$⊢ (((φ \land x \in ℝ^{*}) \land \neg x \in ℝ) \land B < x) \to φ$
10		simpllr	$⊢ (((φ \land x \in ℝ^{}) \land \neg x \in ℝ) \land B < x) \to x \in ℝ^{}$
11		simplr	$⊢ (((φ \land x \in ℝ^{*}) \land \neg x \in ℝ) \land B < x) \to \neg x \in ℝ$
12		mnfxr	$⊢ −∞ \in ℝ^{*}$
13	12	a1i	$⊢ ((φ \land x \in ℝ^{}) \land B < x) \to −∞ \in ℝ^{}$
14		simplr	$⊢ ((φ \land x \in ℝ^{}) \land B < x) \to x \in ℝ^{}$
15	4	ad2antrr	$⊢ ((φ \land x \in ℝ^{}) \land B < x) \to B \in ℝ^{}$
16		mnfle	$⊢ B \in ℝ^{*} \to −∞ \leq B$
17	4 16	syl	$⊢ φ \to −∞ \leq B$
18	17	ad2antrr	$⊢ ((φ \land x \in ℝ^{*}) \land B < x) \to −∞ \leq B$
19		simpr	$⊢ ((φ \land x \in ℝ^{*}) \land B < x) \to B < x$
20	13 15 14 18 19	xrlelttrd	$⊢ ((φ \land x \in ℝ^{*}) \land B < x) \to −∞ < x$
21	13 14 20	xrgtned	$⊢ ((φ \land x \in ℝ^{*}) \land B < x) \to x \neq −∞$
22	21	adantlr	$⊢ (((φ \land x \in ℝ^{*}) \land \neg x \in ℝ) \land B < x) \to x \neq −∞$
23	10 11 22	xrnmnfpnf	$⊢ (((φ \land x \in ℝ^{*}) \land \neg x \in ℝ) \land B < x) \to x = +∞$
24		simpr	$⊢ (((φ \land x \in ℝ^{*}) \land \neg x \in ℝ) \land B < x) \to B < x$
25		simpl	$⊢ (φ \land B = −∞) \to φ$
26		id	$⊢ B = −∞ \to B = −∞$
27		1re	$⊢ 1 \in ℝ$
28		mnflt	$⊢ 1 \in ℝ \to −∞ < 1$
29	27 28	ax-mp	$⊢ −∞ < 1$
30	26 29	eqbrtrdi	$⊢ B = −∞ \to B < 1$
31	30	adantl	$⊢ (φ \land B = −∞) \to B < 1$
32		1red	$⊢ φ \to 1 \in ℝ$
33		breq2	$⊢ x = 1 \to (B < x \leftrightarrow B < 1)$
34		breq2	$⊢ x = 1 \to (y < x \leftrightarrow y < 1)$
35	34	rexbidv	$⊢ x = 1 \to (\exists y \in A y < x \leftrightarrow \exists y \in A y < 1)$
36	33 35	imbi12d	$⊢ x = 1 \to ((B < x \to \exists y \in A y < x) \leftrightarrow (B < 1 \to \exists y \in A y < 1))$
37	36	rspcva	$⊢ (1 \in ℝ \land \forall x \in ℝ (B < x \to \exists y \in A y < x)) \to (B < 1 \to \exists y \in A y < 1)$
38	32 6 37	syl2anc	$⊢ φ \to (B < 1 \to \exists y \in A y < 1)$
39	25 31 38	sylc	$⊢ (φ \land B = −∞) \to \exists y \in A y < 1$
40	39	adantlr	$⊢ ((φ \land x = +∞) \land B = −∞) \to \exists y \in A y < 1$
41		nfv	$⊢ Ⅎ y x = +∞$
42	2 41	nfan	$⊢ Ⅎ y (φ \land x = +∞)$
43	3	sselda	$⊢ (φ \land y \in A) \to y \in ℝ^{*}$
44	43	ad4ant13	$⊢ (((φ \land x = +∞) \land y \in A) \land y < 1) \to y \in ℝ^{*}$
45		1xr	$⊢ 1 \in ℝ^{*}$
46	45	a1i	$⊢ (((φ \land x = +∞) \land y \in A) \land y < 1) \to 1 \in ℝ^{*}$
47		id	$⊢ x = +∞ \to x = +∞$
48		pnfxr	$⊢ +∞ \in ℝ^{*}$
49	47 48	eqeltrdi	$⊢ x = +∞ \to x \in ℝ^{*}$
50	49	adantl	$⊢ (φ \land x = +∞) \to x \in ℝ^{*}$
51	50	ad2antrr	$⊢ (((φ \land x = +∞) \land y \in A) \land y < 1) \to x \in ℝ^{*}$
52		simpr	$⊢ (((φ \land x = +∞) \land y \in A) \land y < 1) \to y < 1$
53		ltpnf	$⊢ 1 \in ℝ \to 1 < +∞$
54	27 53	ax-mp	$⊢ 1 < +∞$
55	54	a1i	$⊢ x = +∞ \to 1 < +∞$
56	47	eqcomd	$⊢ x = +∞ \to +∞ = x$
57	55 56	breqtrd	$⊢ x = +∞ \to 1 < x$
58	57	adantl	$⊢ (φ \land x = +∞) \to 1 < x$
59	58	ad2antrr	$⊢ (((φ \land x = +∞) \land y \in A) \land y < 1) \to 1 < x$
60	44 46 51 52 59	xrlttrd	$⊢ (((φ \land x = +∞) \land y \in A) \land y < 1) \to y < x$
61	60	ex	$⊢ ((φ \land x = +∞) \land y \in A) \to (y < 1 \to y < x)$
62	61	ex	$⊢ (φ \land x = +∞) \to (y \in A \to (y < 1 \to y < x))$
63	42 62	reximdai	$⊢ (φ \land x = +∞) \to (\exists y \in A y < 1 \to \exists y \in A y < x)$
64	63	adantr	$⊢ ((φ \land x = +∞) \land B = −∞) \to (\exists y \in A y < 1 \to \exists y \in A y < x)$
65	40 64	mpd	$⊢ ((φ \land x = +∞) \land B = −∞) \to \exists y \in A y < x$
66	65	3adantl3	$⊢ ((φ \land x = +∞ \land B < x) \land B = −∞) \to \exists y \in A y < x$
67	4	adantr	$⊢ (φ \land \neg B = −∞) \to B \in ℝ^{*}$
68	67	3ad2antl1	$⊢ ((φ \land x = +∞ \land B < x) \land \neg B = −∞) \to B \in ℝ^{*}$
69	26	necon3bi	$⊢ \neg B = −∞ \to B \neq −∞$
70	69	adantl	$⊢ ((φ \land x = +∞ \land B < x) \land \neg B = −∞) \to B \neq −∞$
71	48	a1i	$⊢ ((φ \land x = +∞ \land B < x) \land \neg B = −∞) \to +∞ \in ℝ^{*}$
72		simpr	$⊢ (x = +∞ \land B < x) \to B < x$
73		simpl	$⊢ (x = +∞ \land B < x) \to x = +∞$
74	72 73	breqtrd	$⊢ (x = +∞ \land B < x) \to B < +∞$
75	74	3adant1	$⊢ (φ \land x = +∞ \land B < x) \to B < +∞$
76	75	adantr	$⊢ ((φ \land x = +∞ \land B < x) \land \neg B = −∞) \to B < +∞$
77	68 71 76	xrltned	$⊢ ((φ \land x = +∞ \land B < x) \land \neg B = −∞) \to B \neq +∞$
78	68 70 77	xrred	$⊢ ((φ \land x = +∞ \land B < x) \land \neg B = −∞) \to B \in ℝ$
79	27	a1i	$⊢ ((φ \land x = +∞ \land B < x) \land \neg B = −∞) \to 1 \in ℝ$
80	78 79	readdcld	$⊢ ((φ \land x = +∞ \land B < x) \land \neg B = −∞) \to B + 1 \in ℝ$
81	6	adantr	$⊢ (φ \land \neg B = −∞) \to \forall x \in ℝ (B < x \to \exists y \in A y < x)$
82	81	3ad2antl1	$⊢ ((φ \land x = +∞ \land B < x) \land \neg B = −∞) \to \forall x \in ℝ (B < x \to \exists y \in A y < x)$
83	80 82	jca	$⊢ ((φ \land x = +∞ \land B < x) \land \neg B = −∞) \to (B + 1 \in ℝ \land \forall x \in ℝ (B < x \to \exists y \in A y < x))$
84	78	ltp1d	$⊢ ((φ \land x = +∞ \land B < x) \land \neg B = −∞) \to B < B + 1$
85		breq2	$⊢ x = B + 1 \to (B < x \leftrightarrow B < B + 1)$
86		breq2	$⊢ x = B + 1 \to (y < x \leftrightarrow y < B + 1)$
87	86	rexbidv	$⊢ x = B + 1 \to (\exists y \in A y < x \leftrightarrow \exists y \in A y < B + 1)$
88	85 87	imbi12d	$⊢ x = B + 1 \to ((B < x \to \exists y \in A y < x) \leftrightarrow (B < B + 1 \to \exists y \in A y < B + 1))$
89	88	rspcva	$⊢ (B + 1 \in ℝ \land \forall x \in ℝ (B < x \to \exists y \in A y < x)) \to (B < B + 1 \to \exists y \in A y < B + 1)$
90	83 84 89	sylc	$⊢ ((φ \land x = +∞ \land B < x) \land \neg B = −∞) \to \exists y \in A y < B + 1$
91		nfv	$⊢ Ⅎ y B < x$
92	2 41 91	nf3an	$⊢ Ⅎ y (φ \land x = +∞ \land B < x)$
93		nfv	$⊢ Ⅎ y \neg B = −∞$
94	92 93	nfan	$⊢ Ⅎ y ((φ \land x = +∞ \land B < x) \land \neg B = −∞)$
95	43	3ad2antl1	$⊢ ((φ \land x = +∞ \land B < x) \land y \in A) \to y \in ℝ^{*}$
96	95	ad4ant13	$⊢ ((((φ \land x = +∞ \land B < x) \land \neg B = −∞) \land y \in A) \land y < B + 1) \to y \in ℝ^{*}$
97	80	adantr	$⊢ (((φ \land x = +∞ \land B < x) \land \neg B = −∞) \land y \in A) \to B + 1 \in ℝ$
98	97	rexrd	$⊢ (((φ \land x = +∞ \land B < x) \land \neg B = −∞) \land y \in A) \to B + 1 \in ℝ^{*}$
99	98	adantr	$⊢ ((((φ \land x = +∞ \land B < x) \land \neg B = −∞) \land y \in A) \land y < B + 1) \to B + 1 \in ℝ^{*}$
100	50	3adant3	$⊢ (φ \land x = +∞ \land B < x) \to x \in ℝ^{*}$
101	100	ad3antrrr	$⊢ ((((φ \land x = +∞ \land B < x) \land \neg B = −∞) \land y \in A) \land y < B + 1) \to x \in ℝ^{*}$
102		simpr	$⊢ ((((φ \land x = +∞ \land B < x) \land \neg B = −∞) \land y \in A) \land y < B + 1) \to y < B + 1$
103	80	ltpnfd	$⊢ ((φ \land x = +∞ \land B < x) \land \neg B = −∞) \to B + 1 < +∞$
104	56	adantr	$⊢ (x = +∞ \land \neg B = −∞) \to +∞ = x$
105	104	3ad2antl2	$⊢ ((φ \land x = +∞ \land B < x) \land \neg B = −∞) \to +∞ = x$
106	103 105	breqtrd	$⊢ ((φ \land x = +∞ \land B < x) \land \neg B = −∞) \to B + 1 < x$
107	106	ad2antrr	$⊢ ((((φ \land x = +∞ \land B < x) \land \neg B = −∞) \land y \in A) \land y < B + 1) \to B + 1 < x$
108	96 99 101 102 107	xrlttrd	$⊢ ((((φ \land x = +∞ \land B < x) \land \neg B = −∞) \land y \in A) \land y < B + 1) \to y < x$
109	108	ex	$⊢ (((φ \land x = +∞ \land B < x) \land \neg B = −∞) \land y \in A) \to (y < B + 1 \to y < x)$
110	109	ex	$⊢ ((φ \land x = +∞ \land B < x) \land \neg B = −∞) \to (y \in A \to (y < B + 1 \to y < x))$
111	94 110	reximdai	$⊢ ((φ \land x = +∞ \land B < x) \land \neg B = −∞) \to (\exists y \in A y < B + 1 \to \exists y \in A y < x)$
112	90 111	mpd	$⊢ ((φ \land x = +∞ \land B < x) \land \neg B = −∞) \to \exists y \in A y < x$
113	66 112	pm2.61dan	$⊢ (φ \land x = +∞ \land B < x) \to \exists y \in A y < x$
114	9 23 24 113	syl3anc	$⊢ (((φ \land x \in ℝ^{*}) \land \neg x \in ℝ) \land B < x) \to \exists y \in A y < x$
115	114	ex	$⊢ ((φ \land x \in ℝ^{*}) \land \neg x \in ℝ) \to (B < x \to \exists y \in A y < x)$
116	8 115	pm2.61dan	$⊢ (φ \land x \in ℝ^{*}) \to (B < x \to \exists y \in A y < x)$
117	116	ex	$⊢ φ \to (x \in ℝ^{*} \to (B < x \to \exists y \in A y < x))$
118	1 117	ralrimi	$⊢ φ \to \forall x \in ℝ^{*} (B < x \to \exists y \in A y < x)$
119		xrltso	$⊢ < Or ℝ^{*}$
120	119	a1i	$⊢ ⊤ \to < Or ℝ^{*}$
121	120	eqinf	$⊢ ⊤ \to ((B \in ℝ^{} \land \forall x \in A \neg x < B \land \forall x \in ℝ^{} (B < x \to \exists y \in A y < x)) \to inf (A ℝ^{*} <) = B)$
122	121	mptru	$⊢ (B \in ℝ^{} \land \forall x \in A \neg x < B \land \forall x \in ℝ^{} (B < x \to \exists y \in A y < x)) \to inf (A ℝ^{*} <) = B$
123	4 5 118 122	syl3anc	$⊢ φ \to inf (A ℝ^{*} <) = B$

Metamath Proof Explorer

Theorem infxr

Proof