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

Theorem infxr 44587
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
StepHypRef Expression
1 infxr.b . 2 (𝜑𝐵 ∈ ℝ*)
2 infxr.n . 2 (𝜑 → ∀𝑥𝐴 ¬ 𝑥 < 𝐵)
3 infxr.x . . 3 𝑥𝜑
4 infxr.e . . . . . . 7 (𝜑 → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥))
54r19.21bi 3240 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥))
65adantlr 712 . . . . 5 (((𝜑𝑥 ∈ ℝ*) ∧ 𝑥 ∈ ℝ) → (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥))
7 simplll 772 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝜑)
8 simpllr 773 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 ∈ ℝ*)
9 simplr 766 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → ¬ 𝑥 ∈ ℝ)
10 mnfxr 11269 . . . . . . . . . . 11 -∞ ∈ ℝ*
1110a1i 11 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ*) ∧ 𝐵 < 𝑥) → -∞ ∈ ℝ*)
12 simplr 766 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ*) ∧ 𝐵 < 𝑥) → 𝑥 ∈ ℝ*)
131ad2antrr 723 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ*) ∧ 𝐵 < 𝑥) → 𝐵 ∈ ℝ*)
14 mnfle 13112 . . . . . . . . . . . . 13 (𝐵 ∈ ℝ* → -∞ ≤ 𝐵)
151, 14syl 17 . . . . . . . . . . . 12 (𝜑 → -∞ ≤ 𝐵)
1615ad2antrr 723 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ*) ∧ 𝐵 < 𝑥) → -∞ ≤ 𝐵)
17 simpr 484 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ*) ∧ 𝐵 < 𝑥) → 𝐵 < 𝑥)
1811, 13, 12, 16, 17xrlelttrd 13137 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ*) ∧ 𝐵 < 𝑥) → -∞ < 𝑥)
1911, 12, 18xrgtned 44542 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ*) ∧ 𝐵 < 𝑥) → 𝑥 ≠ -∞)
2019adantlr 712 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 ≠ -∞)
218, 9, 20xrnmnfpnf 44285 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 = +∞)
22 simpr 484 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝐵 < 𝑥)
23 simpl 482 . . . . . . . . . . . 12 ((𝜑𝐵 = -∞) → 𝜑)
24 id 22 . . . . . . . . . . . . . 14 (𝐵 = -∞ → 𝐵 = -∞)
25 1re 11212 . . . . . . . . . . . . . . 15 1 ∈ ℝ
26 mnflt 13101 . . . . . . . . . . . . . . 15 (1 ∈ ℝ → -∞ < 1)
2725, 26ax-mp 5 . . . . . . . . . . . . . 14 -∞ < 1
2824, 27eqbrtrdi 5178 . . . . . . . . . . . . 13 (𝐵 = -∞ → 𝐵 < 1)
2928adantl 481 . . . . . . . . . . . 12 ((𝜑𝐵 = -∞) → 𝐵 < 1)
30 1red 11213 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ ℝ)
31 breq2 5143 . . . . . . . . . . . . . . 15 (𝑥 = 1 → (𝐵 < 𝑥𝐵 < 1))
32 breq2 5143 . . . . . . . . . . . . . . . 16 (𝑥 = 1 → (𝑦 < 𝑥𝑦 < 1))
3332rexbidv 3170 . . . . . . . . . . . . . . 15 (𝑥 = 1 → (∃𝑦𝐴 𝑦 < 𝑥 ↔ ∃𝑦𝐴 𝑦 < 1))
3431, 33imbi12d 344 . . . . . . . . . . . . . 14 (𝑥 = 1 → ((𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥) ↔ (𝐵 < 1 → ∃𝑦𝐴 𝑦 < 1)))
3534rspcva 3602 . . . . . . . . . . . . 13 ((1 ∈ ℝ ∧ ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥)) → (𝐵 < 1 → ∃𝑦𝐴 𝑦 < 1))
3630, 4, 35syl2anc 583 . . . . . . . . . . . 12 (𝜑 → (𝐵 < 1 → ∃𝑦𝐴 𝑦 < 1))
3723, 29, 36sylc 65 . . . . . . . . . . 11 ((𝜑𝐵 = -∞) → ∃𝑦𝐴 𝑦 < 1)
3837adantlr 712 . . . . . . . . . 10 (((𝜑𝑥 = +∞) ∧ 𝐵 = -∞) → ∃𝑦𝐴 𝑦 < 1)
39 infxr.y . . . . . . . . . . . . 13 𝑦𝜑
40 nfv 1909 . . . . . . . . . . . . 13 𝑦 𝑥 = +∞
4139, 40nfan 1894 . . . . . . . . . . . 12 𝑦(𝜑𝑥 = +∞)
42 infxr.a . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ⊆ ℝ*)
4342sselda 3975 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴) → 𝑦 ∈ ℝ*)
4443ad4ant13 748 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 = +∞) ∧ 𝑦𝐴) ∧ 𝑦 < 1) → 𝑦 ∈ ℝ*)
45 1xr 11271 . . . . . . . . . . . . . . . 16 1 ∈ ℝ*
4645a1i 11 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 = +∞) ∧ 𝑦𝐴) ∧ 𝑦 < 1) → 1 ∈ ℝ*)
47 id 22 . . . . . . . . . . . . . . . . . 18 (𝑥 = +∞ → 𝑥 = +∞)
48 pnfxr 11266 . . . . . . . . . . . . . . . . . 18 +∞ ∈ ℝ*
4947, 48eqeltrdi 2833 . . . . . . . . . . . . . . . . 17 (𝑥 = +∞ → 𝑥 ∈ ℝ*)
5049adantl 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 = +∞) → 𝑥 ∈ ℝ*)
5150ad2antrr 723 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 = +∞) ∧ 𝑦𝐴) ∧ 𝑦 < 1) → 𝑥 ∈ ℝ*)
52 simpr 484 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 = +∞) ∧ 𝑦𝐴) ∧ 𝑦 < 1) → 𝑦 < 1)
53 ltpnf 13098 . . . . . . . . . . . . . . . . . . . 20 (1 ∈ ℝ → 1 < +∞)
5425, 53ax-mp 5 . . . . . . . . . . . . . . . . . . 19 1 < +∞
5554a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 = +∞ → 1 < +∞)
5647eqcomd 2730 . . . . . . . . . . . . . . . . . 18 (𝑥 = +∞ → +∞ = 𝑥)
5755, 56breqtrd 5165 . . . . . . . . . . . . . . . . 17 (𝑥 = +∞ → 1 < 𝑥)
5857adantl 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 = +∞) → 1 < 𝑥)
5958ad2antrr 723 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 = +∞) ∧ 𝑦𝐴) ∧ 𝑦 < 1) → 1 < 𝑥)
6044, 46, 51, 52, 59xrlttrd 13136 . . . . . . . . . . . . . 14 ((((𝜑𝑥 = +∞) ∧ 𝑦𝐴) ∧ 𝑦 < 1) → 𝑦 < 𝑥)
6160ex 412 . . . . . . . . . . . . 13 (((𝜑𝑥 = +∞) ∧ 𝑦𝐴) → (𝑦 < 1 → 𝑦 < 𝑥))
6261ex 412 . . . . . . . . . . . 12 ((𝜑𝑥 = +∞) → (𝑦𝐴 → (𝑦 < 1 → 𝑦 < 𝑥)))
6341, 62reximdai 3250 . . . . . . . . . . 11 ((𝜑𝑥 = +∞) → (∃𝑦𝐴 𝑦 < 1 → ∃𝑦𝐴 𝑦 < 𝑥))
6463adantr 480 . . . . . . . . . 10 (((𝜑𝑥 = +∞) ∧ 𝐵 = -∞) → (∃𝑦𝐴 𝑦 < 1 → ∃𝑦𝐴 𝑦 < 𝑥))
6538, 64mpd 15 . . . . . . . . 9 (((𝜑𝑥 = +∞) ∧ 𝐵 = -∞) → ∃𝑦𝐴 𝑦 < 𝑥)
66653adantl3 1165 . . . . . . . 8 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ 𝐵 = -∞) → ∃𝑦𝐴 𝑦 < 𝑥)
671adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐵 = -∞) → 𝐵 ∈ ℝ*)
68673ad2antl1 1182 . . . . . . . . . . . . 13 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ∈ ℝ*)
6924necon3bi 2959 . . . . . . . . . . . . . 14 𝐵 = -∞ → 𝐵 ≠ -∞)
7069adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ≠ -∞)
7148a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → +∞ ∈ ℝ*)
72 simpr 484 . . . . . . . . . . . . . . . . 17 ((𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝐵 < 𝑥)
73 simpl 482 . . . . . . . . . . . . . . . . 17 ((𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝑥 = +∞)
7472, 73breqtrd 5165 . . . . . . . . . . . . . . . 16 ((𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝐵 < +∞)
75743adant1 1127 . . . . . . . . . . . . . . 15 ((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝐵 < +∞)
7675adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 < +∞)
7768, 71, 76xrltned 44577 . . . . . . . . . . . . 13 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ≠ +∞)
7868, 70, 77xrred 44585 . . . . . . . . . . . 12 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ∈ ℝ)
7925a1i 11 . . . . . . . . . . . 12 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 1 ∈ ℝ)
8078, 79readdcld 11241 . . . . . . . . . . 11 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) ∈ ℝ)
814adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐵 = -∞) → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥))
82813ad2antl1 1182 . . . . . . . . . . 11 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥))
8380, 82jca 511 . . . . . . . . . 10 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ((𝐵 + 1) ∈ ℝ ∧ ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥)))
8478ltp1d 12142 . . . . . . . . . 10 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 < (𝐵 + 1))
85 breq2 5143 . . . . . . . . . . . 12 (𝑥 = (𝐵 + 1) → (𝐵 < 𝑥𝐵 < (𝐵 + 1)))
86 breq2 5143 . . . . . . . . . . . . 13 (𝑥 = (𝐵 + 1) → (𝑦 < 𝑥𝑦 < (𝐵 + 1)))
8786rexbidv 3170 . . . . . . . . . . . 12 (𝑥 = (𝐵 + 1) → (∃𝑦𝐴 𝑦 < 𝑥 ↔ ∃𝑦𝐴 𝑦 < (𝐵 + 1)))
8885, 87imbi12d 344 . . . . . . . . . . 11 (𝑥 = (𝐵 + 1) → ((𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥) ↔ (𝐵 < (𝐵 + 1) → ∃𝑦𝐴 𝑦 < (𝐵 + 1))))
8988rspcva 3602 . . . . . . . . . 10 (((𝐵 + 1) ∈ ℝ ∧ ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥)) → (𝐵 < (𝐵 + 1) → ∃𝑦𝐴 𝑦 < (𝐵 + 1)))
9083, 84, 89sylc 65 . . . . . . . . 9 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ∃𝑦𝐴 𝑦 < (𝐵 + 1))
91 nfv 1909 . . . . . . . . . . . 12 𝑦 𝐵 < 𝑥
9239, 40, 91nf3an 1896 . . . . . . . . . . 11 𝑦(𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥)
93 nfv 1909 . . . . . . . . . . 11 𝑦 ¬ 𝐵 = -∞
9492, 93nfan 1894 . . . . . . . . . 10 𝑦((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞)
95433ad2antl1 1182 . . . . . . . . . . . . . 14 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ 𝑦𝐴) → 𝑦 ∈ ℝ*)
9695ad4ant13 748 . . . . . . . . . . . . 13 (((((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑦 ∈ ℝ*)
9780adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦𝐴) → (𝐵 + 1) ∈ ℝ)
9897rexrd 11262 . . . . . . . . . . . . . 14 ((((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦𝐴) → (𝐵 + 1) ∈ ℝ*)
9998adantr 480 . . . . . . . . . . . . 13 (((((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦𝐴) ∧ 𝑦 < (𝐵 + 1)) → (𝐵 + 1) ∈ ℝ*)
100503adant3 1129 . . . . . . . . . . . . . 14 ((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝑥 ∈ ℝ*)
101100ad3antrrr 727 . . . . . . . . . . . . 13 (((((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑥 ∈ ℝ*)
102 simpr 484 . . . . . . . . . . . . 13 (((((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑦 < (𝐵 + 1))
10380ltpnfd 13099 . . . . . . . . . . . . . . 15 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) < +∞)
10456adantr 480 . . . . . . . . . . . . . . . 16 ((𝑥 = +∞ ∧ ¬ 𝐵 = -∞) → +∞ = 𝑥)
1051043ad2antl2 1183 . . . . . . . . . . . . . . 15 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → +∞ = 𝑥)
106103, 105breqtrd 5165 . . . . . . . . . . . . . 14 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) < 𝑥)
107106ad2antrr 723 . . . . . . . . . . . . 13 (((((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦𝐴) ∧ 𝑦 < (𝐵 + 1)) → (𝐵 + 1) < 𝑥)
10896, 99, 101, 102, 107xrlttrd 13136 . . . . . . . . . . . 12 (((((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑦 < 𝑥)
109108ex 412 . . . . . . . . . . 11 ((((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦𝐴) → (𝑦 < (𝐵 + 1) → 𝑦 < 𝑥))
110109ex 412 . . . . . . . . . 10 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝑦𝐴 → (𝑦 < (𝐵 + 1) → 𝑦 < 𝑥)))
11194, 110reximdai 3250 . . . . . . . . 9 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (∃𝑦𝐴 𝑦 < (𝐵 + 1) → ∃𝑦𝐴 𝑦 < 𝑥))
11290, 111mpd 15 . . . . . . . 8 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ∃𝑦𝐴 𝑦 < 𝑥)
11366, 112pm2.61dan 810 . . . . . . 7 ((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) → ∃𝑦𝐴 𝑦 < 𝑥)
1147, 21, 22, 113syl3anc 1368 . . . . . 6 ((((𝜑𝑥 ∈ ℝ*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → ∃𝑦𝐴 𝑦 < 𝑥)
115114ex 412 . . . . 5 (((𝜑𝑥 ∈ ℝ*) ∧ ¬ 𝑥 ∈ ℝ) → (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥))
1166, 115pm2.61dan 810 . . . 4 ((𝜑𝑥 ∈ ℝ*) → (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥))
117116ex 412 . . 3 (𝜑 → (𝑥 ∈ ℝ* → (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥)))
1183, 117ralrimi 3246 . 2 (𝜑 → ∀𝑥 ∈ ℝ* (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥))
119 xrltso 13118 . . . . 5 < Or ℝ*
120119a1i 11 . . . 4 (⊤ → < Or ℝ*)
121120eqinf 9476 . . 3 (⊤ → ((𝐵 ∈ ℝ* ∧ ∀𝑥𝐴 ¬ 𝑥 < 𝐵 ∧ ∀𝑥 ∈ ℝ* (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥)) → inf(𝐴, ℝ*, < ) = 𝐵))
122121mptru 1540 . 2 ((𝐵 ∈ ℝ* ∧ ∀𝑥𝐴 ¬ 𝑥 < 𝐵 ∧ ∀𝑥 ∈ ℝ* (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥)) → inf(𝐴, ℝ*, < ) = 𝐵)
1231, 2, 118, 122syl3anc 1368 1 (𝜑 → inf(𝐴, ℝ*, < ) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  w3a 1084   = wceq 1533  wtru 1534  wnf 1777  wcel 2098  wne 2932  wral 3053  wrex 3062  wss 3941   class class class wbr 5139   Or wor 5578  (class class class)co 7402  infcinf 9433  cr 11106  1c1 11108   + caddc 11110  +∞cpnf 11243  -∞cmnf 11244  *cxr 11245   < clt 11246  cle 11247
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-opab 5202  df-mpt 5223  df-id 5565  df-po 5579  df-so 5580  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7358  df-ov 7405  df-oprab 7406  df-mpo 7407  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-sup 9434  df-inf 9435  df-pnf 11248  df-mnf 11249  df-xr 11250  df-ltxr 11251  df-le 11252  df-sub 11444  df-neg 11445
This theorem is referenced by:  infxrunb2  44588
  Copyright terms: Public domain W3C validator