infxr - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > infxr		Structured version Visualization version GIF version

Theorem infxr 46300

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

**Hypotheses**
Ref	Expression
infxr.x	⊢ Ⅎ𝑥𝜑
infxr.y	⊢ Ⅎ𝑦𝜑
infxr.a	⊢ (𝜑 → 𝐴 ⊆ ℝ^*)
infxr.b	⊢ (𝜑 → 𝐵 ∈ ℝ^*)
infxr.n	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵)
infxr.e	⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))

**Assertion**
Ref	Expression
infxr	⊢ (𝜑 → inf(𝐴, ℝ^*, < ) = 𝐵)

Distinct variable groups: 𝑥,𝐴,𝑦 𝑥,𝐵,𝑦 Allowed substitution hints: 𝜑(𝑥, 𝑦)

**Proof of Theorem infxr**
Step	Hyp	Ref	Expression
1		infxr.b	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
2		infxr.n	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵)
3		infxr.x	. . 3 ⊢ Ⅎ𝑥𝜑
4		infxr.e	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
5	4	r19.21bi 3254	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
6	5	adantlr 728	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝑥 ∈ ℝ) → (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
7		simplll 787	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝜑)
8		simpllr 788	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 ∈ ℝ^)
9		simplr 781	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → ¬ 𝑥 ∈ ℝ)
10		mnfxr 11338	. . . . . . . . . . 11 ⊢ -∞ ∈ ℝ^*
11	10	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^) ∧ 𝐵 < 𝑥) → -∞ ∈ ℝ^)
12		simplr 781	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^) ∧ 𝐵 < 𝑥) → 𝑥 ∈ ℝ^)
13	1	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^) ∧ 𝐵 < 𝑥) → 𝐵 ∈ ℝ^)
14		mnfle 13234	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ℝ^* → -∞ ≤ 𝐵)
15	1, 14	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → -∞ ≤ 𝐵)
16	15	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝐵 < 𝑥) → -∞ ≤ 𝐵)
17		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝐵 < 𝑥) → 𝐵 < 𝑥)
18	11, 13, 12, 16, 17	xrlelttrd 13259	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝐵 < 𝑥) → -∞ < 𝑥)
19	11, 12, 18	xrgtned 13263	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝐵 < 𝑥) → 𝑥 ≠ -∞)
20	19	adantlr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 ≠ -∞)
21	8, 9, 20	xrnmnfpnf 46021	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 = +∞)
22		simpr 490	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝐵 < 𝑥)
23		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = -∞) → 𝜑)
24		id 23	. . . . . . . . . . . . . 14 ⊢ (𝐵 = -∞ → 𝐵 = -∞)
25		1re 11280	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
26		mnflt 13222	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ ℝ → -∞ < 1)
27	25, 26	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ -∞ < 1
28	24, 27	eqbrtrdi 5143	. . . . . . . . . . . . 13 ⊢ (𝐵 = -∞ → 𝐵 < 1)
29	28	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = -∞) → 𝐵 < 1)
30		1red 11281	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ ℝ)
31		breq2 5106	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 1 → (𝐵 < 𝑥 ↔ 𝐵 < 1))
32		breq2 5106	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 1 → (𝑦 < 𝑥 ↔ 𝑦 < 1))
33	32	rexbidv 3186	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 1 → (∃𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑦 < 1))
34	31, 33	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → ((𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥) ↔ (𝐵 < 1 → ∃𝑦 ∈ 𝐴 𝑦 < 1)))
35	34	rspcva 3574	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℝ ∧ ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) → (𝐵 < 1 → ∃𝑦 ∈ 𝐴 𝑦 < 1))
36	30, 4, 35	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 < 1 → ∃𝑦 ∈ 𝐴 𝑦 < 1))
37	23, 29, 36	sylc 66	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = -∞) → ∃𝑦 ∈ 𝐴 𝑦 < 1)
38	37	adantlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 = +∞) ∧ 𝐵 = -∞) → ∃𝑦 ∈ 𝐴 𝑦 < 1)
39		infxr.y	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦𝜑
40		nfv 1947	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 𝑥 = +∞
41	39, 40	nfan 1932	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑥 = +∞)
42		infxr.a	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ⊆ ℝ^*)
43	42	sselda 3930	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ^*)
44	43	ad4ant13 764	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 𝑦 ∈ ℝ^*)
45		1xr 11340	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℝ^*
46	45	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 1 ∈ ℝ^*)
47		id 23	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = +∞ → 𝑥 = +∞)
48		pnfxr 11335	. . . . . . . . . . . . . . . . . 18 ⊢ +∞ ∈ ℝ^*
49	47, 48	eqeltrdi 2868	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = +∞ → 𝑥 ∈ ℝ^*)
50	49	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 = +∞) → 𝑥 ∈ ℝ^*)
51	50	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 𝑥 ∈ ℝ^*)
52		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 𝑦 < 1)
53		ltpnf 13219	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 ∈ ℝ → 1 < +∞)
54	25, 53	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 < +∞
55	54	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = +∞ → 1 < +∞)
56	47	eqcomd 2766	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = +∞ → +∞ = 𝑥)
57	55, 56	breqtrd 5130	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = +∞ → 1 < 𝑥)
58	57	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 = +∞) → 1 < 𝑥)
59	58	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 1 < 𝑥)
60	44, 46, 51, 52, 59	xrlttrd 13258	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 𝑦 < 𝑥)
61	60	ex 418	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) → (𝑦 < 1 → 𝑦 < 𝑥))
62	61	ex 418	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 = +∞) → (𝑦 ∈ 𝐴 → (𝑦 < 1 → 𝑦 < 𝑥)))
63	41, 62	reximdai 3264	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = +∞) → (∃𝑦 ∈ 𝐴 𝑦 < 1 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
64	63	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 = +∞) ∧ 𝐵 = -∞) → (∃𝑦 ∈ 𝐴 𝑦 < 1 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
65	38, 64	mpd 16	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 = +∞) ∧ 𝐵 = -∞) → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)
66	65	3adantl3 1187	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ 𝐵 = -∞) → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)
67	1	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐵 = -∞) → 𝐵 ∈ ℝ^*)
68	67	3ad2antl1 1204	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ∈ ℝ^*)
69	24	necon3bi 2981	. . . . . . . . . . . . . 14 ⊢ (¬ 𝐵 = -∞ → 𝐵 ≠ -∞)
70	69	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ≠ -∞)
71	48	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → +∞ ∈ ℝ^*)
72		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝐵 < 𝑥)
73		simpl 488	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝑥 = +∞)
74	72, 73	breqtrd 5130	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝐵 < +∞)
75	74	3adant1 1148	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝐵 < +∞)
76	75	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 < +∞)
77	68, 71, 76	xrltned 46291	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ≠ +∞)
78	68, 70, 77	xrred 46298	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ∈ ℝ)
79	25	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 1 ∈ ℝ)
80	78, 79	readdcld 11310	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) ∈ ℝ)
81	4	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐵 = -∞) → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
82	81	3ad2antl1 1204	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
83	80, 82	jca 521	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ((𝐵 + 1) ∈ ℝ ∧ ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)))
84	78	ltp1d 12217	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 < (𝐵 + 1))
85		breq2 5106	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐵 + 1) → (𝐵 < 𝑥 ↔ 𝐵 < (𝐵 + 1)))
86		breq2 5106	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐵 + 1) → (𝑦 < 𝑥 ↔ 𝑦 < (𝐵 + 1)))
87	86	rexbidv 3186	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐵 + 1) → (∃𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑦 < (𝐵 + 1)))
88	85, 87	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐵 + 1) → ((𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥) ↔ (𝐵 < (𝐵 + 1) → ∃𝑦 ∈ 𝐴 𝑦 < (𝐵 + 1))))
89	88	rspcva 3574	. . . . . . . . . 10 ⊢ (((𝐵 + 1) ∈ ℝ ∧ ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) → (𝐵 < (𝐵 + 1) → ∃𝑦 ∈ 𝐴 𝑦 < (𝐵 + 1)))
90	83, 84, 89	sylc 66	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ∃𝑦 ∈ 𝐴 𝑦 < (𝐵 + 1))
91		nfv 1947	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝐵 < 𝑥
92	39, 40, 91	nf3an 1934	. . . . . . . . . . 11 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥)
93		nfv 1947	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 ¬ 𝐵 = -∞
94	92, 93	nfan 1932	. . . . . . . . . 10 ⊢ Ⅎ𝑦((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞)
95	43	3ad2antl1 1204	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ^*)
96	95	ad4ant13 764	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑦 ∈ ℝ^*)
97	80	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) → (𝐵 + 1) ∈ ℝ)
98	97	rexrd 11331	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) → (𝐵 + 1) ∈ ℝ^*)
99	98	adantr 486	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → (𝐵 + 1) ∈ ℝ^*)
100	50	3adant3 1150	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝑥 ∈ ℝ^*)
101	100	ad3antrrr 743	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑥 ∈ ℝ^*)
102		simpr 490	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑦 < (𝐵 + 1))
103	80	ltpnfd 13220	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) < +∞)
104	56	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = +∞ ∧ ¬ 𝐵 = -∞) → +∞ = 𝑥)
105	104	3ad2antl2 1205	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → +∞ = 𝑥)
106	103, 105	breqtrd 5130	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) < 𝑥)
107	106	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → (𝐵 + 1) < 𝑥)
108	96, 99, 101, 102, 107	xrlttrd 13258	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑦 < 𝑥)
109	108	ex 418	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) → (𝑦 < (𝐵 + 1) → 𝑦 < 𝑥))
110	109	ex 418	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝑦 ∈ 𝐴 → (𝑦 < (𝐵 + 1) → 𝑦 < 𝑥)))
111	94, 110	reximdai 3264	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (∃𝑦 ∈ 𝐴 𝑦 < (𝐵 + 1) → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
112	90, 111	mpd 16	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)
113	66, 112	pm2.61dan 825	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)
114	7, 21, 22, 113	syl3anc 1398	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)
115	114	ex 418	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) → (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
116	6, 115	pm2.61dan 825	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ^*) → (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
117	116	ex 418	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ^* → (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)))
118	3, 117	ralrimi 3260	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ℝ^* (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
119		xrltso 13240	. . . . 5 ⊢ < Or ℝ^*
120	119	a1i 11	. . . 4 ⊢ (⊤ → < Or ℝ^*)
121	120	eqinf 9455	. . 3 ⊢ (⊤ → ((𝐵 ∈ ℝ^* ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵 ∧ ∀𝑥 ∈ ℝ^* (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) → inf(𝐴, ℝ^*, < ) = 𝐵))
122	121	mptru 1577	. 2 ⊢ ((𝐵 ∈ ℝ^* ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵 ∧ ∀𝑥 ∈ ℝ^* (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) → inf(𝐴, ℝ^*, < ) = 𝐵)
123	1, 2, 118, 122	syl3anc 1398	1 ⊢ (𝜑 → inf(𝐴, ℝ^*, < ) = 𝐵)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ⊤wtru 1571 Ⅎwnf 1816 ∈ wcel 2145 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 ⊆ wss 3898 class class class wbr 5102 Or wor 5554 (class class class)co 7408 infcinf 9411 ℝcr 11171 1c1 11173 + caddc 11175 +∞cpnf 11312 -∞cmnf 11313 ℝ^*cxr 11314 < clt 11315 ≤ cle 11316

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7734 ax-cnex 11228 ax-resscn 11229 ax-1cn 11230 ax-icn 11231 ax-addcl 11232 ax-addrcl 11233 ax-mulcl 11234 ax-mulrcl 11235 ax-mulcom 11236 ax-addass 11237 ax-mulass 11238 ax-distr 11239 ax-i2m1 11240 ax-1ne0 11241 ax-1rid 11242 ax-rnegex 11243 ax-rrecex 11244 ax-cnre 11245 ax-pre-lttri 11246 ax-pre-lttrn 11247 ax-pre-ltadd 11248 ax-pre-mulgt0 11249

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5542 df-po 5555 df-so 5556 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-iota 6483 df-fun 6529 df-fn 6530 df-f 6531 df-f1 6532 df-fo 6533 df-f1o 6534 df-fv 6535 df-riota 7365 df-ov 7411 df-oprab 7412 df-mpo 7413 df-er 8695 df-en 8952 df-dom 8953 df-sdom 8954 df-sup 9412 df-inf 9413 df-pnf 11317 df-mnf 11318 df-xr 11319 df-ltxr 11320 df-le 11321 df-sub 11515 df-neg 11516

This theorem is used by: infxrunb2 46301

W3C validator