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 45384

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 3222	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
6	5	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝑥 ∈ ℝ) → (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
7		simplll 774	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝜑)
8		simpllr 775	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 ∈ ℝ^)
9		simplr 768	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → ¬ 𝑥 ∈ ℝ)
10		mnfxr 11161	. . . . . . . . . . 11 ⊢ -∞ ∈ ℝ^*
11	10	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^) ∧ 𝐵 < 𝑥) → -∞ ∈ ℝ^)
12		simplr 768	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^) ∧ 𝐵 < 𝑥) → 𝑥 ∈ ℝ^)
13	1	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^) ∧ 𝐵 < 𝑥) → 𝐵 ∈ ℝ^)
14		mnfle 13026	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ℝ^* → -∞ ≤ 𝐵)
15	1, 14	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → -∞ ≤ 𝐵)
16	15	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝐵 < 𝑥) → -∞ ≤ 𝐵)
17		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝐵 < 𝑥) → 𝐵 < 𝑥)
18	11, 13, 12, 16, 17	xrlelttrd 13051	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝐵 < 𝑥) → -∞ < 𝑥)
19	11, 12, 18	xrgtned 45340	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝐵 < 𝑥) → 𝑥 ≠ -∞)
20	19	adantlr 715	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 ≠ -∞)
21	8, 9, 20	xrnmnfpnf 45099	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 = +∞)
22		simpr 484	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝐵 < 𝑥)
23		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = -∞) → 𝜑)
24		id 22	. . . . . . . . . . . . . 14 ⊢ (𝐵 = -∞ → 𝐵 = -∞)
25		1re 11104	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
26		mnflt 13014	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ ℝ → -∞ < 1)
27	25, 26	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ -∞ < 1
28	24, 27	eqbrtrdi 5128	. . . . . . . . . . . . 13 ⊢ (𝐵 = -∞ → 𝐵 < 1)
29	28	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = -∞) → 𝐵 < 1)
30		1red 11105	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ ℝ)
31		breq2 5093	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 1 → (𝐵 < 𝑥 ↔ 𝐵 < 1))
32		breq2 5093	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 1 → (𝑦 < 𝑥 ↔ 𝑦 < 1))
33	32	rexbidv 3154	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 1 → (∃𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑦 < 1))
34	31, 33	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → ((𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥) ↔ (𝐵 < 1 → ∃𝑦 ∈ 𝐴 𝑦 < 1)))
35	34	rspcva 3573	. . . . . . . . . . . . 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 1915	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 𝑥 = +∞
41	39, 40	nfan 1900	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑥 = +∞)
42		infxr.a	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ⊆ ℝ^*)
43	42	sselda 3932	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ^*)
44	43	ad4ant13 751	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 𝑦 ∈ ℝ^*)
45		1xr 11163	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℝ^*
46	45	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 1 ∈ ℝ^*)
47		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = +∞ → 𝑥 = +∞)
48		pnfxr 11158	. . . . . . . . . . . . . . . . . 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 13011	. . . . . . . . . . . . . . . . . . . 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 5115	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = +∞ → 1 < 𝑥)
58	57	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 = +∞) → 1 < 𝑥)
59	58	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 1 < 𝑥)
60	44, 46, 51, 52, 59	xrlttrd 13050	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 𝑦 < 𝑥)
61	60	ex 412	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) → (𝑦 < 1 → 𝑦 < 𝑥))
62	61	ex 412	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 = +∞) → (𝑦 ∈ 𝐴 → (𝑦 < 1 → 𝑦 < 𝑥)))
63	41, 62	reximdai 3232	. . . . . . . . . . 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 5115	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝐵 < +∞)
75	74	3adant1 1130	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝐵 < +∞)
76	75	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 < +∞)
77	68, 71, 76	xrltned 45375	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ≠ +∞)
78	68, 70, 77	xrred 45382	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ∈ ℝ)
79	25	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 1 ∈ ℝ)
80	78, 79	readdcld 11133	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) ∈ ℝ)
81	4	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐵 = -∞) → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
82	81	3ad2antl1 1186	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
83	80, 82	jca 511	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ((𝐵 + 1) ∈ ℝ ∧ ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)))
84	78	ltp1d 12044	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 < (𝐵 + 1))
85		breq2 5093	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐵 + 1) → (𝐵 < 𝑥 ↔ 𝐵 < (𝐵 + 1)))
86		breq2 5093	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐵 + 1) → (𝑦 < 𝑥 ↔ 𝑦 < (𝐵 + 1)))
87	86	rexbidv 3154	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐵 + 1) → (∃𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑦 < (𝐵 + 1)))
88	85, 87	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐵 + 1) → ((𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥) ↔ (𝐵 < (𝐵 + 1) → ∃𝑦 ∈ 𝐴 𝑦 < (𝐵 + 1))))
89	88	rspcva 3573	. . . . . . . . . 10 ⊢ (((𝐵 + 1) ∈ ℝ ∧ ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) → (𝐵 < (𝐵 + 1) → ∃𝑦 ∈ 𝐴 𝑦 < (𝐵 + 1)))
90	83, 84, 89	sylc 65	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ∃𝑦 ∈ 𝐴 𝑦 < (𝐵 + 1))
91		nfv 1915	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝐵 < 𝑥
92	39, 40, 91	nf3an 1902	. . . . . . . . . . 11 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥)
93		nfv 1915	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 ¬ 𝐵 = -∞
94	92, 93	nfan 1900	. . . . . . . . . 10 ⊢ Ⅎ𝑦((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞)
95	43	3ad2antl1 1186	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ^*)
96	95	ad4ant13 751	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑦 ∈ ℝ^*)
97	80	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) → (𝐵 + 1) ∈ ℝ)
98	97	rexrd 11154	. . . . . . . . . . . . . 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 13012	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) < +∞)
104	56	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = +∞ ∧ ¬ 𝐵 = -∞) → +∞ = 𝑥)
105	104	3ad2antl2 1187	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → +∞ = 𝑥)
106	103, 105	breqtrd 5115	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) < 𝑥)
107	106	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → (𝐵 + 1) < 𝑥)
108	96, 99, 101, 102, 107	xrlttrd 13050	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑦 < 𝑥)
109	108	ex 412	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) → (𝑦 < (𝐵 + 1) → 𝑦 < 𝑥))
110	109	ex 412	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝑦 ∈ 𝐴 → (𝑦 < (𝐵 + 1) → 𝑦 < 𝑥)))
111	94, 110	reximdai 3232	. . . . . . . . 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 3228	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ℝ^* (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
119		xrltso 13032	. . . . 5 ⊢ < Or ℝ^*
120	119	a1i 11	. . . 4 ⊢ (⊤ → < Or ℝ^*)
121	120	eqinf 9364	. . 3 ⊢ (⊤ → ((𝐵 ∈ ℝ^* ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵 ∧ ∀𝑥 ∈ ℝ^* (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) → inf(𝐴, ℝ^*, < ) = 𝐵))
122	121	mptru 1548	. 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 1541 ⊤wtru 1542 Ⅎwnf 1784 ∈ wcel 2110 ≠ wne 2926 ∀wral 3045 ∃wrex 3054 ⊆ wss 3900 class class class wbr 5089 Or wor 5521 (class class class)co 7341 infcinf 9320 ℝcr 10997 1c1 10999 + caddc 11001 +∞cpnf 11135 -∞cmnf 11136 ℝ^*cxr 11137 < clt 11138 ≤ cle 11139

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2112 ax-9 2120 ax-10 2143 ax-11 2159 ax-12 2179 ax-ext 2702 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7663 ax-cnex 11054 ax-resscn 11055 ax-1cn 11056 ax-icn 11057 ax-addcl 11058 ax-addrcl 11059 ax-mulcl 11060 ax-mulrcl 11061 ax-mulcom 11062 ax-addass 11063 ax-mulass 11064 ax-distr 11065 ax-i2m1 11066 ax-1ne0 11067 ax-1rid 11068 ax-rnegex 11069 ax-rrecex 11070 ax-cnre 11071 ax-pre-lttri 11072 ax-pre-lttrn 11073 ax-pre-ltadd 11074 ax-pre-mulgt0 11075

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2067 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 3344 df-reu 3345 df-rab 3394 df-v 3436 df-sbc 3740 df-csb 3849 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-nul 4282 df-if 4474 df-pw 4550 df-sn 4575 df-pr 4577 df-op 4581 df-uni 4858 df-br 5090 df-opab 5152 df-mpt 5171 df-id 5509 df-po 5522 df-so 5523 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-iota 6433 df-fun 6479 df-fn 6480 df-f 6481 df-f1 6482 df-fo 6483 df-f1o 6484 df-fv 6485 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-er 8617 df-en 8865 df-dom 8866 df-sdom 8867 df-sup 9321 df-inf 9322 df-pnf 11140 df-mnf 11141 df-xr 11142 df-ltxr 11143 df-le 11144 df-sub 11338 df-neg 11339

This theorem is referenced by: infxrunb2 45385

W3C validator