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 45394

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 3234	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
6	5	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝑥 ∈ ℝ) → (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
7		simplll 774	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝜑)
8		simpllr 775	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 ∈ ℝ^)
9		simplr 768	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → ¬ 𝑥 ∈ ℝ)
10		mnfxr 11292	. . . . . . . . . . 11 ⊢ -∞ ∈ ℝ^*
11	10	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^) ∧ 𝐵 < 𝑥) → -∞ ∈ ℝ^)
12		simplr 768	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^) ∧ 𝐵 < 𝑥) → 𝑥 ∈ ℝ^)
13	1	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^) ∧ 𝐵 < 𝑥) → 𝐵 ∈ ℝ^)
14		mnfle 13151	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ℝ^* → -∞ ≤ 𝐵)
15	1, 14	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → -∞ ≤ 𝐵)
16	15	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝐵 < 𝑥) → -∞ ≤ 𝐵)
17		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝐵 < 𝑥) → 𝐵 < 𝑥)
18	11, 13, 12, 16, 17	xrlelttrd 13176	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝐵 < 𝑥) → -∞ < 𝑥)
19	11, 12, 18	xrgtned 45349	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝐵 < 𝑥) → 𝑥 ≠ -∞)
20	19	adantlr 715	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 ≠ -∞)
21	8, 9, 20	xrnmnfpnf 45107	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 = +∞)
22		simpr 484	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝐵 < 𝑥)
23		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = -∞) → 𝜑)
24		id 22	. . . . . . . . . . . . . 14 ⊢ (𝐵 = -∞ → 𝐵 = -∞)
25		1re 11235	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
26		mnflt 13139	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ ℝ → -∞ < 1)
27	25, 26	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ -∞ < 1
28	24, 27	eqbrtrdi 5158	. . . . . . . . . . . . 13 ⊢ (𝐵 = -∞ → 𝐵 < 1)
29	28	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = -∞) → 𝐵 < 1)
30		1red 11236	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ ℝ)
31		breq2 5123	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 1 → (𝐵 < 𝑥 ↔ 𝐵 < 1))
32		breq2 5123	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 1 → (𝑦 < 𝑥 ↔ 𝑦 < 1))
33	32	rexbidv 3164	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 1 → (∃𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑦 < 1))
34	31, 33	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → ((𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥) ↔ (𝐵 < 1 → ∃𝑦 ∈ 𝐴 𝑦 < 1)))
35	34	rspcva 3599	. . . . . . . . . . . . 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 3958	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ^*)
44	43	ad4ant13 751	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 𝑦 ∈ ℝ^*)
45		1xr 11294	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℝ^*
46	45	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 1 ∈ ℝ^*)
47		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = +∞ → 𝑥 = +∞)
48		pnfxr 11289	. . . . . . . . . . . . . . . . . 18 ⊢ +∞ ∈ ℝ^*
49	47, 48	eqeltrdi 2842	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = +∞ → 𝑥 ∈ ℝ^*)
50	49	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 = +∞) → 𝑥 ∈ ℝ^*)
51	50	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 𝑥 ∈ ℝ^*)
52		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 𝑦 < 1)
53		ltpnf 13136	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 ∈ ℝ → 1 < +∞)
54	25, 53	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 < +∞
55	54	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = +∞ → 1 < +∞)
56	47	eqcomd 2741	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = +∞ → +∞ = 𝑥)
57	55, 56	breqtrd 5145	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = +∞ → 1 < 𝑥)
58	57	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 = +∞) → 1 < 𝑥)
59	58	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 1 < 𝑥)
60	44, 46, 51, 52, 59	xrlttrd 13175	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 𝑦 < 𝑥)
61	60	ex 412	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) → (𝑦 < 1 → 𝑦 < 𝑥))
62	61	ex 412	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 = +∞) → (𝑦 ∈ 𝐴 → (𝑦 < 1 → 𝑦 < 𝑥)))
63	41, 62	reximdai 3244	. . . . . . . . . . 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 2958	. . . . . . . . . . . . . 14 ⊢ (¬ 𝐵 = -∞ → 𝐵 ≠ -∞)
70	69	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ≠ -∞)
71	48	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → +∞ ∈ ℝ^*)
72		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝐵 < 𝑥)
73		simpl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝑥 = +∞)
74	72, 73	breqtrd 5145	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝐵 < +∞)
75	74	3adant1 1130	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝐵 < +∞)
76	75	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 < +∞)
77	68, 71, 76	xrltned 45384	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ≠ +∞)
78	68, 70, 77	xrred 45392	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ∈ ℝ)
79	25	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 1 ∈ ℝ)
80	78, 79	readdcld 11264	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) ∈ ℝ)
81	4	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐵 = -∞) → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
82	81	3ad2antl1 1186	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
83	80, 82	jca 511	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ((𝐵 + 1) ∈ ℝ ∧ ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)))
84	78	ltp1d 12172	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 < (𝐵 + 1))
85		breq2 5123	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐵 + 1) → (𝐵 < 𝑥 ↔ 𝐵 < (𝐵 + 1)))
86		breq2 5123	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐵 + 1) → (𝑦 < 𝑥 ↔ 𝑦 < (𝐵 + 1)))
87	86	rexbidv 3164	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐵 + 1) → (∃𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑦 < (𝐵 + 1)))
88	85, 87	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐵 + 1) → ((𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥) ↔ (𝐵 < (𝐵 + 1) → ∃𝑦 ∈ 𝐴 𝑦 < (𝐵 + 1))))
89	88	rspcva 3599	. . . . . . . . . 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 11285	. . . . . . . . . . . . . 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 13137	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) < +∞)
104	56	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = +∞ ∧ ¬ 𝐵 = -∞) → +∞ = 𝑥)
105	104	3ad2antl2 1187	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → +∞ = 𝑥)
106	103, 105	breqtrd 5145	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) < 𝑥)
107	106	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → (𝐵 + 1) < 𝑥)
108	96, 99, 101, 102, 107	xrlttrd 13175	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑦 < 𝑥)
109	108	ex 412	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) → (𝑦 < (𝐵 + 1) → 𝑦 < 𝑥))
110	109	ex 412	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝑦 ∈ 𝐴 → (𝑦 < (𝐵 + 1) → 𝑦 < 𝑥)))
111	94, 110	reximdai 3244	. . . . . . . . 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 3240	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ℝ^* (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
119		xrltso 13157	. . . . 5 ⊢ < Or ℝ^*
120	119	a1i 11	. . . 4 ⊢ (⊤ → < Or ℝ^*)
121	120	eqinf 9497	. . 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 2108 ≠ wne 2932 ∀wral 3051 ∃wrex 3060 ⊆ wss 3926 class class class wbr 5119 Or wor 5560 (class class class)co 7405 infcinf 9453 ℝcr 11128 1c1 11130 + caddc 11132 +∞cpnf 11266 -∞cmnf 11267 ℝ^*cxr 11268 < clt 11269 ≤ cle 11270

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 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729 ax-cnex 11185 ax-resscn 11186 ax-1cn 11187 ax-icn 11188 ax-addcl 11189 ax-addrcl 11190 ax-mulcl 11191 ax-mulrcl 11192 ax-mulcom 11193 ax-addass 11194 ax-mulass 11195 ax-distr 11196 ax-i2m1 11197 ax-1ne0 11198 ax-1rid 11199 ax-rnegex 11200 ax-rrecex 11201 ax-cnre 11202 ax-pre-lttri 11203 ax-pre-lttrn 11204 ax-pre-ltadd 11205 ax-pre-mulgt0 11206

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 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3359 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-br 5120 df-opab 5182 df-mpt 5202 df-id 5548 df-po 5561 df-so 5562 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7362 df-ov 7408 df-oprab 7409 df-mpo 7410 df-er 8719 df-en 8960 df-dom 8961 df-sdom 8962 df-sup 9454 df-inf 9455 df-pnf 11271 df-mnf 11272 df-xr 11273 df-ltxr 11274 df-le 11275 df-sub 11468 df-neg 11469

This theorem is referenced by: infxrunb2 45395

W3C validator