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 46198

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 3256	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
6	5	adantlr 728	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝑥 ∈ ℝ) → (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
7		simplll 787	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝜑)
8		simpllr 788	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 ∈ ℝ^)
9		simplr 781	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → ¬ 𝑥 ∈ ℝ)
10		mnfxr 11293	. . . . . . . . . . 11 ⊢ -∞ ∈ ℝ^*
11	10	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^) ∧ 𝐵 < 𝑥) → -∞ ∈ ℝ^)
12		simplr 781	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^) ∧ 𝐵 < 𝑥) → 𝑥 ∈ ℝ^)
13	1	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^) ∧ 𝐵 < 𝑥) → 𝐵 ∈ ℝ^)
14		mnfle 13188	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ℝ^* → -∞ ≤ 𝐵)
15	1, 14	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → -∞ ≤ 𝐵)
16	15	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝐵 < 𝑥) → -∞ ≤ 𝐵)
17		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝐵 < 𝑥) → 𝐵 < 𝑥)
18	11, 13, 12, 16, 17	xrlelttrd 13213	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝐵 < 𝑥) → -∞ < 𝑥)
19	11, 12, 18	xrgtned 13217	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ 𝐵 < 𝑥) → 𝑥 ≠ -∞)
20	19	adantlr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 ≠ -∞)
21	8, 9, 20	xrnmnfpnf 45919	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 = +∞)
22		simpr 490	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ^*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝐵 < 𝑥)
23		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = -∞) → 𝜑)
24		id 23	. . . . . . . . . . . . . 14 ⊢ (𝐵 = -∞ → 𝐵 = -∞)
25		1re 11235	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
26		mnflt 13176	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ ℝ → -∞ < 1)
27	25, 26	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ -∞ < 1
28	24, 27	eqbrtrdi 5148	. . . . . . . . . . . . 13 ⊢ (𝐵 = -∞ → 𝐵 < 1)
29	28	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = -∞) → 𝐵 < 1)
30		1red 11236	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ ℝ)
31		breq2 5111	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 1 → (𝐵 < 𝑥 ↔ 𝐵 < 1))
32		breq2 5111	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 1 → (𝑦 < 𝑥 ↔ 𝑦 < 1))
33	32	rexbidv 3188	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 1 → (∃𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑦 < 1))
34	31, 33	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → ((𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥) ↔ (𝐵 < 1 → ∃𝑦 ∈ 𝐴 𝑦 < 1)))
35	34	rspcva 3577	. . . . . . . . . . . . 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 3934	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ^*)
44	43	ad4ant13 764	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 𝑦 ∈ ℝ^*)
45		1xr 11295	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℝ^*
46	45	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 1 ∈ ℝ^*)
47		id 23	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = +∞ → 𝑥 = +∞)
48		pnfxr 11290	. . . . . . . . . . . . . . . . . 18 ⊢ +∞ ∈ ℝ^*
49	47, 48	eqeltrdi 2870	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = +∞ → 𝑥 ∈ ℝ^*)
50	49	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 = +∞) → 𝑥 ∈ ℝ^*)
51	50	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 𝑥 ∈ ℝ^*)
52		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 𝑦 < 1)
53		ltpnf 13173	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 ∈ ℝ → 1 < +∞)
54	25, 53	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 < +∞
55	54	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = +∞ → 1 < +∞)
56	47	eqcomd 2768	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = +∞ → +∞ = 𝑥)
57	55, 56	breqtrd 5135	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = +∞ → 1 < 𝑥)
58	57	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 = +∞) → 1 < 𝑥)
59	58	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 1 < 𝑥)
60	44, 46, 51, 52, 59	xrlttrd 13212	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 𝑦 < 𝑥)
61	60	ex 418	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) → (𝑦 < 1 → 𝑦 < 𝑥))
62	61	ex 418	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 = +∞) → (𝑦 ∈ 𝐴 → (𝑦 < 1 → 𝑦 < 𝑥)))
63	41, 62	reximdai 3266	. . . . . . . . . . 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 2983	. . . . . . . . . . . . . 14 ⊢ (¬ 𝐵 = -∞ → 𝐵 ≠ -∞)
70	69	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ≠ -∞)
71	48	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → +∞ ∈ ℝ^*)
72		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝐵 < 𝑥)
73		simpl 488	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝑥 = +∞)
74	72, 73	breqtrd 5135	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝐵 < +∞)
75	74	3adant1 1148	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝐵 < +∞)
76	75	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 < +∞)
77	68, 71, 76	xrltned 46189	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ≠ +∞)
78	68, 70, 77	xrred 46196	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ∈ ℝ)
79	25	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 1 ∈ ℝ)
80	78, 79	readdcld 11265	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) ∈ ℝ)
81	4	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐵 = -∞) → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
82	81	3ad2antl1 1204	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
83	80, 82	jca 521	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ((𝐵 + 1) ∈ ℝ ∧ ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)))
84	78	ltp1d 12172	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 < (𝐵 + 1))
85		breq2 5111	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐵 + 1) → (𝐵 < 𝑥 ↔ 𝐵 < (𝐵 + 1)))
86		breq2 5111	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐵 + 1) → (𝑦 < 𝑥 ↔ 𝑦 < (𝐵 + 1)))
87	86	rexbidv 3188	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐵 + 1) → (∃𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑦 < (𝐵 + 1)))
88	85, 87	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐵 + 1) → ((𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥) ↔ (𝐵 < (𝐵 + 1) → ∃𝑦 ∈ 𝐴 𝑦 < (𝐵 + 1))))
89	88	rspcva 3577	. . . . . . . . . 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 11286	. . . . . . . . . . . . . 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 13174	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) < +∞)
104	56	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = +∞ ∧ ¬ 𝐵 = -∞) → +∞ = 𝑥)
105	104	3ad2antl2 1205	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → +∞ = 𝑥)
106	103, 105	breqtrd 5135	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) < 𝑥)
107	106	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → (𝐵 + 1) < 𝑥)
108	96, 99, 101, 102, 107	xrlttrd 13212	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑦 < 𝑥)
109	108	ex 418	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) → (𝑦 < (𝐵 + 1) → 𝑦 < 𝑥))
110	109	ex 418	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝑦 ∈ 𝐴 → (𝑦 < (𝐵 + 1) → 𝑦 < 𝑥)))
111	94, 110	reximdai 3266	. . . . . . . . 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 3262	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ℝ^* (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))
119		xrltso 13194	. . . . 5 ⊢ < Or ℝ^*
120	119	a1i 11	. . . 4 ⊢ (⊤ → < Or ℝ^*)
121	120	eqinf 9458	. . 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 2957 ∀wral 3078 ∃wrex 3088 ⊆ wss 3902 class class class wbr 5107 Or wor 5566 (class class class)co 7416 infcinf 9414 ℝcr 11126 1c1 11128 + caddc 11130 +∞cpnf 11267 -∞cmnf 11268 ℝ^*cxr 11269 < clt 11270 ≤ cle 11271

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 2215 ax-ext 2734 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204

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 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-br 5108 df-opab 5172 df-mpt 5191 df-id 5554 df-po 5567 df-so 5568 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-er 8699 df-en 8956 df-dom 8957 df-sdom 8958 df-sup 9415 df-inf 9416 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471

This theorem is used by: infxrunb2 46199

W3C validator