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 45370

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 3230	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
6	5	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝑥 ∈ ℝ) → (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
7		simplll 774	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝜑)
8		simpllr 775	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 ∈ ℝ^)
9		simplr 768	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → ¬ 𝑥 ∈ ℝ)
10		mnfxr 11238	. . . . . . . . . . 11 ⊢ -∞ ∈ ℝ^*
11	10	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^) ∧ 𝐵 < 𝑥) → -∞ ∈ ℝ^)
12		simplr 768	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^) ∧ 𝐵 < 𝑥) → 𝑥 ∈ ℝ^)
13	1	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^) ∧ 𝐵 < 𝑥) → 𝐵 ∈ ℝ^)
14		mnfle 13102	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ℝ^* → -∞ ≤ 𝐵)
15	1, 14	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → -∞ ≤ 𝐵)
16	15	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝐵 < 𝑥) → -∞ ≤ 𝐵)
17		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝐵 < 𝑥) → 𝐵 < 𝑥)
18	11, 13, 12, 16, 17	xrlelttrd 13127	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝐵 < 𝑥) → -∞ < 𝑥)
19	11, 12, 18	xrgtned 45325	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝐵 < 𝑥) → 𝑥 ≠ -∞)
20	19	adantlr 715	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 ≠ -∞)
21	8, 9, 20	xrnmnfpnf 45084	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 = +∞)
22		simpr 484	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝐵 < 𝑥)
23		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = -∞) → 𝜑)
24		id 22	. . . . . . . . . . . . . 14 ⊢ (𝐵 = -∞ → 𝐵 = -∞)
25		1re 11181	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
26		mnflt 13090	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ ℝ → -∞ < 1)
27	25, 26	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ -∞ < 1
28	24, 27	eqbrtrdi 5149	. . . . . . . . . . . . 13 ⊢ (𝐵 = -∞ → 𝐵 < 1)
29	28	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = -∞) → 𝐵 < 1)
30		1red 11182	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ ℝ)
31		breq2 5114	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 1 → (𝐵 < 𝑥 ↔ 𝐵 < 1))
32		breq2 5114	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 1 → (𝑦 < 𝑥 ↔ 𝑦 < 1))
33	32	rexbidv 3158	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 1 → (∃𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑦 < 1))
34	31, 33	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → ((𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥) ↔ (𝐵 < 1 → ∃𝑦 ∈ 𝐴 𝑦 < 1)))
35	34	rspcva 3589	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℝ ∧ ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) → (𝐵 < 1 → ∃𝑦 ∈ 𝐴 𝑦 < 1))
36	30, 4, 35	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 < 1 → ∃𝑦 ∈ 𝐴 𝑦 < 1))
37	23, 29, 36	sylc 65	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = -∞) → ∃𝑦 ∈ 𝐴 𝑦 < 1)
38	37	adantlr 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 = +∞) ∧ 𝐵 = -∞) → ∃𝑦 ∈ 𝐴 𝑦 < 1)
39		infxr.y	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦𝜑
40		nfv 1914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 𝑥 = +∞
41	39, 40	nfan 1899	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑥 = +∞)
42		infxr.a	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ⊆ ℝ^*)
43	42	sselda 3949	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ^*)
44	43	ad4ant13 751	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 𝑦 ∈ ℝ^*)
45		1xr 11240	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℝ^*
46	45	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 1 ∈ ℝ^*)
47		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = +∞ → 𝑥 = +∞)
48		pnfxr 11235	. . . . . . . . . . . . . . . . . 18 ⊢ +∞ ∈ ℝ^*
49	47, 48	eqeltrdi 2837	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = +∞ → 𝑥 ∈ ℝ^*)
50	49	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 = +∞) → 𝑥 ∈ ℝ^*)
51	50	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 𝑥 ∈ ℝ^*)
52		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 𝑦 < 1)
53		ltpnf 13087	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 ∈ ℝ → 1 < +∞)
54	25, 53	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 < +∞
55	54	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = +∞ → 1 < +∞)
56	47	eqcomd 2736	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = +∞ → +∞ = 𝑥)
57	55, 56	breqtrd 5136	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = +∞ → 1 < 𝑥)
58	57	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 = +∞) → 1 < 𝑥)
59	58	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 1 < 𝑥)
60	44, 46, 51, 52, 59	xrlttrd 13126	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 𝑦 < 𝑥)
61	60	ex 412	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) → (𝑦 < 1 → 𝑦 < 𝑥))
62	61	ex 412	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 = +∞) → (𝑦 ∈ 𝐴 → (𝑦 < 1 → 𝑦 < 𝑥)))
63	41, 62	reximdai 3240	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = +∞) → (∃𝑦 ∈ 𝐴 𝑦 < 1 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
64	63	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 = +∞) ∧ 𝐵 = -∞) → (∃𝑦 ∈ 𝐴 𝑦 < 1 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
65	38, 64	mpd 15	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 = +∞) ∧ 𝐵 = -∞) → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)
66	65	3adantl3 1169	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ 𝐵 = -∞) → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)
67	1	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐵 = -∞) → 𝐵 ∈ ℝ^*)
68	67	3ad2antl1 1186	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ∈ ℝ^*)
69	24	necon3bi 2952	. . . . . . . . . . . . . 14 ⊢ (¬ 𝐵 = -∞ → 𝐵 ≠ -∞)
70	69	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ≠ -∞)
71	48	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → +∞ ∈ ℝ^*)
72		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝐵 < 𝑥)
73		simpl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝑥 = +∞)
74	72, 73	breqtrd 5136	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝐵 < +∞)
75	74	3adant1 1130	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝐵 < +∞)
76	75	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 < +∞)
77	68, 71, 76	xrltned 45360	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ≠ +∞)
78	68, 70, 77	xrred 45368	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ∈ ℝ)
79	25	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 1 ∈ ℝ)
80	78, 79	readdcld 11210	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) ∈ ℝ)
81	4	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐵 = -∞) → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
82	81	3ad2antl1 1186	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
83	80, 82	jca 511	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ((𝐵 + 1) ∈ ℝ ∧ ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)))
84	78	ltp1d 12120	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 < (𝐵 + 1))
85		breq2 5114	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐵 + 1) → (𝐵 < 𝑥 ↔ 𝐵 < (𝐵 + 1)))
86		breq2 5114	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐵 + 1) → (𝑦 < 𝑥 ↔ 𝑦 < (𝐵 + 1)))
87	86	rexbidv 3158	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐵 + 1) → (∃𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑦 < (𝐵 + 1)))
88	85, 87	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐵 + 1) → ((𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥) ↔ (𝐵 < (𝐵 + 1) → ∃𝑦 ∈ 𝐴 𝑦 < (𝐵 + 1))))
89	88	rspcva 3589	. . . . . . . . . 10 ⊢ (((𝐵 + 1) ∈ ℝ ∧ ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) → (𝐵 < (𝐵 + 1) → ∃𝑦 ∈ 𝐴 𝑦 < (𝐵 + 1)))
90	83, 84, 89	sylc 65	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ∃𝑦 ∈ 𝐴 𝑦 < (𝐵 + 1))
91		nfv 1914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝐵 < 𝑥
92	39, 40, 91	nf3an 1901	. . . . . . . . . . 11 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥)
93		nfv 1914	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 ¬ 𝐵 = -∞
94	92, 93	nfan 1899	. . . . . . . . . 10 ⊢ Ⅎ𝑦((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞)
95	43	3ad2antl1 1186	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ^*)
96	95	ad4ant13 751	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑦 ∈ ℝ^*)
97	80	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) → (𝐵 + 1) ∈ ℝ)
98	97	rexrd 11231	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) → (𝐵 + 1) ∈ ℝ^*)
99	98	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → (𝐵 + 1) ∈ ℝ^*)
100	50	3adant3 1132	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝑥 ∈ ℝ^*)
101	100	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑥 ∈ ℝ^*)
102		simpr 484	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑦 < (𝐵 + 1))
103	80	ltpnfd 13088	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) < +∞)
104	56	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = +∞ ∧ ¬ 𝐵 = -∞) → +∞ = 𝑥)
105	104	3ad2antl2 1187	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → +∞ = 𝑥)
106	103, 105	breqtrd 5136	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) < 𝑥)
107	106	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → (𝐵 + 1) < 𝑥)
108	96, 99, 101, 102, 107	xrlttrd 13126	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑦 < 𝑥)
109	108	ex 412	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) → (𝑦 < (𝐵 + 1) → 𝑦 < 𝑥))
110	109	ex 412	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝑦 ∈ 𝐴 → (𝑦 < (𝐵 + 1) → 𝑦 < 𝑥)))
111	94, 110	reximdai 3240	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (∃𝑦 ∈ 𝐴 𝑦 < (𝐵 + 1) → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
112	90, 111	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)
113	66, 112	pm2.61dan 812	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)
114	7, 21, 22, 113	syl3anc 1373	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)
115	114	ex 412	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) → (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
116	6, 115	pm2.61dan 812	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ^*) → (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
117	116	ex 412	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ^* → (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)))
118	3, 117	ralrimi 3236	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ℝ^* (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
119		xrltso 13108	. . . . 5 ⊢ < Or ℝ^*
120	119	a1i 11	. . . 4 ⊢ (⊤ → < Or ℝ^*)
121	120	eqinf 9443	. . 3 ⊢ (⊤ → ((𝐵 ∈ ℝ^* ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵 ∧ ∀𝑥 ∈ ℝ^* (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) → inf(𝐴, ℝ^*, < ) = 𝐵))
122	121	mptru 1547	. 2 ⊢ ((𝐵 ∈ ℝ^* ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵 ∧ ∀𝑥 ∈ ℝ^* (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) → inf(𝐴, ℝ^*, < ) = 𝐵)
123	1, 2, 118, 122	syl3anc 1373	1 ⊢ (𝜑 → inf(𝐴, ℝ^*, < ) = 𝐵)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ⊤wtru 1541 Ⅎwnf 1783 ∈ wcel 2109 ≠ wne 2926 ∀wral 3045 ∃wrex 3054 ⊆ wss 3917 class class class wbr 5110 Or wor 5548 (class class class)co 7390 infcinf 9399 ℝcr 11074 1c1 11076 + caddc 11078 +∞cpnf 11212 -∞cmnf 11213 ℝ^*cxr 11214 < clt 11215 ≤ cle 11216

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3356 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-br 5111 df-opab 5173 df-mpt 5192 df-id 5536 df-po 5549 df-so 5550 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-er 8674 df-en 8922 df-dom 8923 df-sdom 8924 df-sup 9400 df-inf 9401 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-sub 11414 df-neg 11415

This theorem is referenced by: infxrunb2 45371

W3C validator