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 43591
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 3234 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥))
65adantlr 713 . . . . 5 (((𝜑𝑥 ∈ ℝ*) ∧ 𝑥 ∈ ℝ) → (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥))
7 simplll 773 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝜑)
8 simpllr 774 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 ∈ ℝ*)
9 simplr 767 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → ¬ 𝑥 ∈ ℝ)
10 mnfxr 11212 . . . . . . . . . . 11 -∞ ∈ ℝ*
1110a1i 11 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ*) ∧ 𝐵 < 𝑥) → -∞ ∈ ℝ*)
12 simplr 767 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ*) ∧ 𝐵 < 𝑥) → 𝑥 ∈ ℝ*)
131ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ*) ∧ 𝐵 < 𝑥) → 𝐵 ∈ ℝ*)
14 mnfle 13055 . . . . . . . . . . . . 13 (𝐵 ∈ ℝ* → -∞ ≤ 𝐵)
151, 14syl 17 . . . . . . . . . . . 12 (𝜑 → -∞ ≤ 𝐵)
1615ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ*) ∧ 𝐵 < 𝑥) → -∞ ≤ 𝐵)
17 simpr 485 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ*) ∧ 𝐵 < 𝑥) → 𝐵 < 𝑥)
1811, 13, 12, 16, 17xrlelttrd 13079 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ*) ∧ 𝐵 < 𝑥) → -∞ < 𝑥)
1911, 12, 18xrgtned 43546 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ*) ∧ 𝐵 < 𝑥) → 𝑥 ≠ -∞)
2019adantlr 713 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 ≠ -∞)
218, 9, 20xrnmnfpnf 43283 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝑥 = +∞)
22 simpr 485 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → 𝐵 < 𝑥)
23 simpl 483 . . . . . . . . . . . 12 ((𝜑𝐵 = -∞) → 𝜑)
24 id 22 . . . . . . . . . . . . . 14 (𝐵 = -∞ → 𝐵 = -∞)
25 1re 11155 . . . . . . . . . . . . . . 15 1 ∈ ℝ
26 mnflt 13044 . . . . . . . . . . . . . . 15 (1 ∈ ℝ → -∞ < 1)
2725, 26ax-mp 5 . . . . . . . . . . . . . 14 -∞ < 1
2824, 27eqbrtrdi 5144 . . . . . . . . . . . . 13 (𝐵 = -∞ → 𝐵 < 1)
2928adantl 482 . . . . . . . . . . . 12 ((𝜑𝐵 = -∞) → 𝐵 < 1)
30 1red 11156 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ ℝ)
31 breq2 5109 . . . . . . . . . . . . . . 15 (𝑥 = 1 → (𝐵 < 𝑥𝐵 < 1))
32 breq2 5109 . . . . . . . . . . . . . . . 16 (𝑥 = 1 → (𝑦 < 𝑥𝑦 < 1))
3332rexbidv 3175 . . . . . . . . . . . . . . 15 (𝑥 = 1 → (∃𝑦𝐴 𝑦 < 𝑥 ↔ ∃𝑦𝐴 𝑦 < 1))
3431, 33imbi12d 344 . . . . . . . . . . . . . 14 (𝑥 = 1 → ((𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥) ↔ (𝐵 < 1 → ∃𝑦𝐴 𝑦 < 1)))
3534rspcva 3579 . . . . . . . . . . . . 13 ((1 ∈ ℝ ∧ ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥)) → (𝐵 < 1 → ∃𝑦𝐴 𝑦 < 1))
3630, 4, 35syl2anc 584 . . . . . . . . . . . 12 (𝜑 → (𝐵 < 1 → ∃𝑦𝐴 𝑦 < 1))
3723, 29, 36sylc 65 . . . . . . . . . . 11 ((𝜑𝐵 = -∞) → ∃𝑦𝐴 𝑦 < 1)
3837adantlr 713 . . . . . . . . . 10 (((𝜑𝑥 = +∞) ∧ 𝐵 = -∞) → ∃𝑦𝐴 𝑦 < 1)
39 infxr.y . . . . . . . . . . . . 13 𝑦𝜑
40 nfv 1917 . . . . . . . . . . . . 13 𝑦 𝑥 = +∞
4139, 40nfan 1902 . . . . . . . . . . . 12 𝑦(𝜑𝑥 = +∞)
42 infxr.a . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ⊆ ℝ*)
4342sselda 3944 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴) → 𝑦 ∈ ℝ*)
4443ad4ant13 749 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 = +∞) ∧ 𝑦𝐴) ∧ 𝑦 < 1) → 𝑦 ∈ ℝ*)
45 1xr 11214 . . . . . . . . . . . . . . . 16 1 ∈ ℝ*
4645a1i 11 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 = +∞) ∧ 𝑦𝐴) ∧ 𝑦 < 1) → 1 ∈ ℝ*)
47 id 22 . . . . . . . . . . . . . . . . . 18 (𝑥 = +∞ → 𝑥 = +∞)
48 pnfxr 11209 . . . . . . . . . . . . . . . . . 18 +∞ ∈ ℝ*
4947, 48eqeltrdi 2846 . . . . . . . . . . . . . . . . 17 (𝑥 = +∞ → 𝑥 ∈ ℝ*)
5049adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 = +∞) → 𝑥 ∈ ℝ*)
5150ad2antrr 724 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 = +∞) ∧ 𝑦𝐴) ∧ 𝑦 < 1) → 𝑥 ∈ ℝ*)
52 simpr 485 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 = +∞) ∧ 𝑦𝐴) ∧ 𝑦 < 1) → 𝑦 < 1)
53 ltpnf 13041 . . . . . . . . . . . . . . . . . . . 20 (1 ∈ ℝ → 1 < +∞)
5425, 53ax-mp 5 . . . . . . . . . . . . . . . . . . 19 1 < +∞
5554a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 = +∞ → 1 < +∞)
5647eqcomd 2742 . . . . . . . . . . . . . . . . . 18 (𝑥 = +∞ → +∞ = 𝑥)
5755, 56breqtrd 5131 . . . . . . . . . . . . . . . . 17 (𝑥 = +∞ → 1 < 𝑥)
5857adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 = +∞) → 1 < 𝑥)
5958ad2antrr 724 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 = +∞) ∧ 𝑦𝐴) ∧ 𝑦 < 1) → 1 < 𝑥)
6044, 46, 51, 52, 59xrlttrd 13078 . . . . . . . . . . . . . 14 ((((𝜑𝑥 = +∞) ∧ 𝑦𝐴) ∧ 𝑦 < 1) → 𝑦 < 𝑥)
6160ex 413 . . . . . . . . . . . . 13 (((𝜑𝑥 = +∞) ∧ 𝑦𝐴) → (𝑦 < 1 → 𝑦 < 𝑥))
6261ex 413 . . . . . . . . . . . 12 ((𝜑𝑥 = +∞) → (𝑦𝐴 → (𝑦 < 1 → 𝑦 < 𝑥)))
6341, 62reximdai 3244 . . . . . . . . . . 11 ((𝜑𝑥 = +∞) → (∃𝑦𝐴 𝑦 < 1 → ∃𝑦𝐴 𝑦 < 𝑥))
6463adantr 481 . . . . . . . . . 10 (((𝜑𝑥 = +∞) ∧ 𝐵 = -∞) → (∃𝑦𝐴 𝑦 < 1 → ∃𝑦𝐴 𝑦 < 𝑥))
6538, 64mpd 15 . . . . . . . . 9 (((𝜑𝑥 = +∞) ∧ 𝐵 = -∞) → ∃𝑦𝐴 𝑦 < 𝑥)
66653adantl3 1168 . . . . . . . 8 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ 𝐵 = -∞) → ∃𝑦𝐴 𝑦 < 𝑥)
671adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐵 = -∞) → 𝐵 ∈ ℝ*)
68673ad2antl1 1185 . . . . . . . . . . . . 13 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ∈ ℝ*)
6924necon3bi 2970 . . . . . . . . . . . . . 14 𝐵 = -∞ → 𝐵 ≠ -∞)
7069adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ≠ -∞)
7148a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → +∞ ∈ ℝ*)
72 simpr 485 . . . . . . . . . . . . . . . . 17 ((𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝐵 < 𝑥)
73 simpl 483 . . . . . . . . . . . . . . . . 17 ((𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝑥 = +∞)
7472, 73breqtrd 5131 . . . . . . . . . . . . . . . 16 ((𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝐵 < +∞)
75743adant1 1130 . . . . . . . . . . . . . . 15 ((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝐵 < +∞)
7675adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 < +∞)
7768, 71, 76xrltned 43581 . . . . . . . . . . . . 13 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ≠ +∞)
7868, 70, 77xrred 43589 . . . . . . . . . . . 12 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ∈ ℝ)
7925a1i 11 . . . . . . . . . . . 12 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 1 ∈ ℝ)
8078, 79readdcld 11184 . . . . . . . . . . 11 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) ∈ ℝ)
814adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐵 = -∞) → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥))
82813ad2antl1 1185 . . . . . . . . . . 11 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥))
8380, 82jca 512 . . . . . . . . . 10 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ((𝐵 + 1) ∈ ℝ ∧ ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥)))
8478ltp1d 12085 . . . . . . . . . 10 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 < (𝐵 + 1))
85 breq2 5109 . . . . . . . . . . . 12 (𝑥 = (𝐵 + 1) → (𝐵 < 𝑥𝐵 < (𝐵 + 1)))
86 breq2 5109 . . . . . . . . . . . . 13 (𝑥 = (𝐵 + 1) → (𝑦 < 𝑥𝑦 < (𝐵 + 1)))
8786rexbidv 3175 . . . . . . . . . . . 12 (𝑥 = (𝐵 + 1) → (∃𝑦𝐴 𝑦 < 𝑥 ↔ ∃𝑦𝐴 𝑦 < (𝐵 + 1)))
8885, 87imbi12d 344 . . . . . . . . . . 11 (𝑥 = (𝐵 + 1) → ((𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥) ↔ (𝐵 < (𝐵 + 1) → ∃𝑦𝐴 𝑦 < (𝐵 + 1))))
8988rspcva 3579 . . . . . . . . . 10 (((𝐵 + 1) ∈ ℝ ∧ ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥)) → (𝐵 < (𝐵 + 1) → ∃𝑦𝐴 𝑦 < (𝐵 + 1)))
9083, 84, 89sylc 65 . . . . . . . . 9 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ∃𝑦𝐴 𝑦 < (𝐵 + 1))
91 nfv 1917 . . . . . . . . . . . 12 𝑦 𝐵 < 𝑥
9239, 40, 91nf3an 1904 . . . . . . . . . . 11 𝑦(𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥)
93 nfv 1917 . . . . . . . . . . 11 𝑦 ¬ 𝐵 = -∞
9492, 93nfan 1902 . . . . . . . . . 10 𝑦((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞)
95433ad2antl1 1185 . . . . . . . . . . . . . 14 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ 𝑦𝐴) → 𝑦 ∈ ℝ*)
9695ad4ant13 749 . . . . . . . . . . . . 13 (((((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑦 ∈ ℝ*)
9780adantr 481 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦𝐴) → (𝐵 + 1) ∈ ℝ)
9897rexrd 11205 . . . . . . . . . . . . . 14 ((((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦𝐴) → (𝐵 + 1) ∈ ℝ*)
9998adantr 481 . . . . . . . . . . . . 13 (((((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦𝐴) ∧ 𝑦 < (𝐵 + 1)) → (𝐵 + 1) ∈ ℝ*)
100503adant3 1132 . . . . . . . . . . . . . 14 ((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝑥 ∈ ℝ*)
101100ad3antrrr 728 . . . . . . . . . . . . 13 (((((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑥 ∈ ℝ*)
102 simpr 485 . . . . . . . . . . . . 13 (((((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑦 < (𝐵 + 1))
10380ltpnfd 13042 . . . . . . . . . . . . . . 15 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) < +∞)
10456adantr 481 . . . . . . . . . . . . . . . 16 ((𝑥 = +∞ ∧ ¬ 𝐵 = -∞) → +∞ = 𝑥)
1051043ad2antl2 1186 . . . . . . . . . . . . . . 15 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → +∞ = 𝑥)
106103, 105breqtrd 5131 . . . . . . . . . . . . . 14 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) < 𝑥)
107106ad2antrr 724 . . . . . . . . . . . . 13 (((((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦𝐴) ∧ 𝑦 < (𝐵 + 1)) → (𝐵 + 1) < 𝑥)
10896, 99, 101, 102, 107xrlttrd 13078 . . . . . . . . . . . 12 (((((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑦 < 𝑥)
109108ex 413 . . . . . . . . . . 11 ((((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦𝐴) → (𝑦 < (𝐵 + 1) → 𝑦 < 𝑥))
110109ex 413 . . . . . . . . . 10 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝑦𝐴 → (𝑦 < (𝐵 + 1) → 𝑦 < 𝑥)))
11194, 110reximdai 3244 . . . . . . . . 9 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (∃𝑦𝐴 𝑦 < (𝐵 + 1) → ∃𝑦𝐴 𝑦 < 𝑥))
11290, 111mpd 15 . . . . . . . 8 (((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ∃𝑦𝐴 𝑦 < 𝑥)
11366, 112pm2.61dan 811 . . . . . . 7 ((𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥) → ∃𝑦𝐴 𝑦 < 𝑥)
1147, 21, 22, 113syl3anc 1371 . . . . . 6 ((((𝜑𝑥 ∈ ℝ*) ∧ ¬ 𝑥 ∈ ℝ) ∧ 𝐵 < 𝑥) → ∃𝑦𝐴 𝑦 < 𝑥)
115114ex 413 . . . . 5 (((𝜑𝑥 ∈ ℝ*) ∧ ¬ 𝑥 ∈ ℝ) → (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥))
1166, 115pm2.61dan 811 . . . 4 ((𝜑𝑥 ∈ ℝ*) → (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥))
117116ex 413 . . 3 (𝜑 → (𝑥 ∈ ℝ* → (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥)))
1183, 117ralrimi 3240 . 2 (𝜑 → ∀𝑥 ∈ ℝ* (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥))
119 xrltso 13060 . . . . 5 < Or ℝ*
120119a1i 11 . . . 4 (⊤ → < Or ℝ*)
121120eqinf 9420 . . 3 (⊤ → ((𝐵 ∈ ℝ* ∧ ∀𝑥𝐴 ¬ 𝑥 < 𝐵 ∧ ∀𝑥 ∈ ℝ* (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥)) → inf(𝐴, ℝ*, < ) = 𝐵))
122121mptru 1548 . 2 ((𝐵 ∈ ℝ* ∧ ∀𝑥𝐴 ¬ 𝑥 < 𝐵 ∧ ∀𝑥 ∈ ℝ* (𝐵 < 𝑥 → ∃𝑦𝐴 𝑦 < 𝑥)) → inf(𝐴, ℝ*, < ) = 𝐵)
1231, 2, 118, 122syl3anc 1371 1 (𝜑 → inf(𝐴, ℝ*, < ) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3a 1087   = wceq 1541  wtru 1542  wnf 1785  wcel 2106  wne 2943  wral 3064  wrex 3073  wss 3910   class class class wbr 5105   Or wor 5544  (class class class)co 7357  infcinf 9377  cr 11050  1c1 11052   + caddc 11054  +∞cpnf 11186  -∞cmnf 11187  *cxr 11188   < clt 11189  cle 11190
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-po 5545  df-so 5546  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-sup 9378  df-inf 9379  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388
This theorem is referenced by:  infxrunb2  43592
  Copyright terms: Public domain W3C validator