Metamath Proof Explorer


Theorem infxr

Description: The infimum of a set of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses infxr.x 𝑥 𝜑
infxr.y 𝑦 𝜑
infxr.a ( 𝜑𝐴 ⊆ ℝ* )
infxr.b ( 𝜑𝐵 ∈ ℝ* )
infxr.n ( 𝜑 → ∀ 𝑥𝐴 ¬ 𝑥 < 𝐵 )
infxr.e ( 𝜑 → ∀ 𝑥 ∈ ℝ ( 𝐵 < 𝑥 → ∃ 𝑦𝐴 𝑦 < 𝑥 ) )
Assertion infxr ( 𝜑 → inf ( 𝐴 , ℝ* , < ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 infxr.x 𝑥 𝜑
2 infxr.y 𝑦 𝜑
3 infxr.a ( 𝜑𝐴 ⊆ ℝ* )
4 infxr.b ( 𝜑𝐵 ∈ ℝ* )
5 infxr.n ( 𝜑 → ∀ 𝑥𝐴 ¬ 𝑥 < 𝐵 )
6 infxr.e ( 𝜑 → ∀ 𝑥 ∈ ℝ ( 𝐵 < 𝑥 → ∃ 𝑦𝐴 𝑦 < 𝑥 ) )
7 6 r19.21bi ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝐵 < 𝑥 → ∃ 𝑦𝐴 𝑦 < 𝑥 ) )
8 7 adantlr ( ( ( 𝜑𝑥 ∈ ℝ* ) ∧ 𝑥 ∈ ℝ ) → ( 𝐵 < 𝑥 → ∃ 𝑦𝐴 𝑦 < 𝑥 ) )
9 simplll ( ( ( ( 𝜑𝑥 ∈ ℝ* ) ∧ ¬ 𝑥 ∈ ℝ ) ∧ 𝐵 < 𝑥 ) → 𝜑 )
10 simpllr ( ( ( ( 𝜑𝑥 ∈ ℝ* ) ∧ ¬ 𝑥 ∈ ℝ ) ∧ 𝐵 < 𝑥 ) → 𝑥 ∈ ℝ* )
11 simplr ( ( ( ( 𝜑𝑥 ∈ ℝ* ) ∧ ¬ 𝑥 ∈ ℝ ) ∧ 𝐵 < 𝑥 ) → ¬ 𝑥 ∈ ℝ )
12 mnfxr -∞ ∈ ℝ*
13 12 a1i ( ( ( 𝜑𝑥 ∈ ℝ* ) ∧ 𝐵 < 𝑥 ) → -∞ ∈ ℝ* )
14 simplr ( ( ( 𝜑𝑥 ∈ ℝ* ) ∧ 𝐵 < 𝑥 ) → 𝑥 ∈ ℝ* )
15 4 ad2antrr ( ( ( 𝜑𝑥 ∈ ℝ* ) ∧ 𝐵 < 𝑥 ) → 𝐵 ∈ ℝ* )
16 mnfle ( 𝐵 ∈ ℝ* → -∞ ≤ 𝐵 )
17 4 16 syl ( 𝜑 → -∞ ≤ 𝐵 )
18 17 ad2antrr ( ( ( 𝜑𝑥 ∈ ℝ* ) ∧ 𝐵 < 𝑥 ) → -∞ ≤ 𝐵 )
19 simpr ( ( ( 𝜑𝑥 ∈ ℝ* ) ∧ 𝐵 < 𝑥 ) → 𝐵 < 𝑥 )
20 13 15 14 18 19 xrlelttrd ( ( ( 𝜑𝑥 ∈ ℝ* ) ∧ 𝐵 < 𝑥 ) → -∞ < 𝑥 )
21 13 14 20 xrgtned ( ( ( 𝜑𝑥 ∈ ℝ* ) ∧ 𝐵 < 𝑥 ) → 𝑥 ≠ -∞ )
22 21 adantlr ( ( ( ( 𝜑𝑥 ∈ ℝ* ) ∧ ¬ 𝑥 ∈ ℝ ) ∧ 𝐵 < 𝑥 ) → 𝑥 ≠ -∞ )
23 10 11 22 xrnmnfpnf ( ( ( ( 𝜑𝑥 ∈ ℝ* ) ∧ ¬ 𝑥 ∈ ℝ ) ∧ 𝐵 < 𝑥 ) → 𝑥 = +∞ )
24 simpr ( ( ( ( 𝜑𝑥 ∈ ℝ* ) ∧ ¬ 𝑥 ∈ ℝ ) ∧ 𝐵 < 𝑥 ) → 𝐵 < 𝑥 )
25 simpl ( ( 𝜑𝐵 = -∞ ) → 𝜑 )
26 id ( 𝐵 = -∞ → 𝐵 = -∞ )
27 1re 1 ∈ ℝ
28 mnflt ( 1 ∈ ℝ → -∞ < 1 )
29 27 28 ax-mp -∞ < 1
30 26 29 eqbrtrdi ( 𝐵 = -∞ → 𝐵 < 1 )
31 30 adantl ( ( 𝜑𝐵 = -∞ ) → 𝐵 < 1 )
32 1red ( 𝜑 → 1 ∈ ℝ )
33 breq2 ( 𝑥 = 1 → ( 𝐵 < 𝑥𝐵 < 1 ) )
34 breq2 ( 𝑥 = 1 → ( 𝑦 < 𝑥𝑦 < 1 ) )
35 34 rexbidv ( 𝑥 = 1 → ( ∃ 𝑦𝐴 𝑦 < 𝑥 ↔ ∃ 𝑦𝐴 𝑦 < 1 ) )
36 33 35 imbi12d ( 𝑥 = 1 → ( ( 𝐵 < 𝑥 → ∃ 𝑦𝐴 𝑦 < 𝑥 ) ↔ ( 𝐵 < 1 → ∃ 𝑦𝐴 𝑦 < 1 ) ) )
37 36 rspcva ( ( 1 ∈ ℝ ∧ ∀ 𝑥 ∈ ℝ ( 𝐵 < 𝑥 → ∃ 𝑦𝐴 𝑦 < 𝑥 ) ) → ( 𝐵 < 1 → ∃ 𝑦𝐴 𝑦 < 1 ) )
38 32 6 37 syl2anc ( 𝜑 → ( 𝐵 < 1 → ∃ 𝑦𝐴 𝑦 < 1 ) )
39 25 31 38 sylc ( ( 𝜑𝐵 = -∞ ) → ∃ 𝑦𝐴 𝑦 < 1 )
40 39 adantlr ( ( ( 𝜑𝑥 = +∞ ) ∧ 𝐵 = -∞ ) → ∃ 𝑦𝐴 𝑦 < 1 )
41 nfv 𝑦 𝑥 = +∞
42 2 41 nfan 𝑦 ( 𝜑𝑥 = +∞ )
43 3 sselda ( ( 𝜑𝑦𝐴 ) → 𝑦 ∈ ℝ* )
44 43 ad4ant13 ( ( ( ( 𝜑𝑥 = +∞ ) ∧ 𝑦𝐴 ) ∧ 𝑦 < 1 ) → 𝑦 ∈ ℝ* )
45 1xr 1 ∈ ℝ*
46 45 a1i ( ( ( ( 𝜑𝑥 = +∞ ) ∧ 𝑦𝐴 ) ∧ 𝑦 < 1 ) → 1 ∈ ℝ* )
47 id ( 𝑥 = +∞ → 𝑥 = +∞ )
48 pnfxr +∞ ∈ ℝ*
49 47 48 eqeltrdi ( 𝑥 = +∞ → 𝑥 ∈ ℝ* )
50 49 adantl ( ( 𝜑𝑥 = +∞ ) → 𝑥 ∈ ℝ* )
51 50 ad2antrr ( ( ( ( 𝜑𝑥 = +∞ ) ∧ 𝑦𝐴 ) ∧ 𝑦 < 1 ) → 𝑥 ∈ ℝ* )
52 simpr ( ( ( ( 𝜑𝑥 = +∞ ) ∧ 𝑦𝐴 ) ∧ 𝑦 < 1 ) → 𝑦 < 1 )
53 ltpnf ( 1 ∈ ℝ → 1 < +∞ )
54 27 53 ax-mp 1 < +∞
55 54 a1i ( 𝑥 = +∞ → 1 < +∞ )
56 47 eqcomd ( 𝑥 = +∞ → +∞ = 𝑥 )
57 55 56 breqtrd ( 𝑥 = +∞ → 1 < 𝑥 )
58 57 adantl ( ( 𝜑𝑥 = +∞ ) → 1 < 𝑥 )
59 58 ad2antrr ( ( ( ( 𝜑𝑥 = +∞ ) ∧ 𝑦𝐴 ) ∧ 𝑦 < 1 ) → 1 < 𝑥 )
60 44 46 51 52 59 xrlttrd ( ( ( ( 𝜑𝑥 = +∞ ) ∧ 𝑦𝐴 ) ∧ 𝑦 < 1 ) → 𝑦 < 𝑥 )
61 60 ex ( ( ( 𝜑𝑥 = +∞ ) ∧ 𝑦𝐴 ) → ( 𝑦 < 1 → 𝑦 < 𝑥 ) )
62 61 ex ( ( 𝜑𝑥 = +∞ ) → ( 𝑦𝐴 → ( 𝑦 < 1 → 𝑦 < 𝑥 ) ) )
63 42 62 reximdai ( ( 𝜑𝑥 = +∞ ) → ( ∃ 𝑦𝐴 𝑦 < 1 → ∃ 𝑦𝐴 𝑦 < 𝑥 ) )
64 63 adantr ( ( ( 𝜑𝑥 = +∞ ) ∧ 𝐵 = -∞ ) → ( ∃ 𝑦𝐴 𝑦 < 1 → ∃ 𝑦𝐴 𝑦 < 𝑥 ) )
65 40 64 mpd ( ( ( 𝜑𝑥 = +∞ ) ∧ 𝐵 = -∞ ) → ∃ 𝑦𝐴 𝑦 < 𝑥 )
66 65 3adantl3 ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ 𝐵 = -∞ ) → ∃ 𝑦𝐴 𝑦 < 𝑥 )
67 4 adantr ( ( 𝜑 ∧ ¬ 𝐵 = -∞ ) → 𝐵 ∈ ℝ* )
68 67 3ad2antl1 ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) → 𝐵 ∈ ℝ* )
69 26 necon3bi ( ¬ 𝐵 = -∞ → 𝐵 ≠ -∞ )
70 69 adantl ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) → 𝐵 ≠ -∞ )
71 48 a1i ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) → +∞ ∈ ℝ* )
72 simpr ( ( 𝑥 = +∞ ∧ 𝐵 < 𝑥 ) → 𝐵 < 𝑥 )
73 simpl ( ( 𝑥 = +∞ ∧ 𝐵 < 𝑥 ) → 𝑥 = +∞ )
74 72 73 breqtrd ( ( 𝑥 = +∞ ∧ 𝐵 < 𝑥 ) → 𝐵 < +∞ )
75 74 3adant1 ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) → 𝐵 < +∞ )
76 75 adantr ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) → 𝐵 < +∞ )
77 68 71 76 xrltned ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) → 𝐵 ≠ +∞ )
78 68 70 77 xrred ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) → 𝐵 ∈ ℝ )
79 27 a1i ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) → 1 ∈ ℝ )
80 78 79 readdcld ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) → ( 𝐵 + 1 ) ∈ ℝ )
81 6 adantr ( ( 𝜑 ∧ ¬ 𝐵 = -∞ ) → ∀ 𝑥 ∈ ℝ ( 𝐵 < 𝑥 → ∃ 𝑦𝐴 𝑦 < 𝑥 ) )
82 81 3ad2antl1 ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) → ∀ 𝑥 ∈ ℝ ( 𝐵 < 𝑥 → ∃ 𝑦𝐴 𝑦 < 𝑥 ) )
83 80 82 jca ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) → ( ( 𝐵 + 1 ) ∈ ℝ ∧ ∀ 𝑥 ∈ ℝ ( 𝐵 < 𝑥 → ∃ 𝑦𝐴 𝑦 < 𝑥 ) ) )
84 78 ltp1d ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) → 𝐵 < ( 𝐵 + 1 ) )
85 breq2 ( 𝑥 = ( 𝐵 + 1 ) → ( 𝐵 < 𝑥𝐵 < ( 𝐵 + 1 ) ) )
86 breq2 ( 𝑥 = ( 𝐵 + 1 ) → ( 𝑦 < 𝑥𝑦 < ( 𝐵 + 1 ) ) )
87 86 rexbidv ( 𝑥 = ( 𝐵 + 1 ) → ( ∃ 𝑦𝐴 𝑦 < 𝑥 ↔ ∃ 𝑦𝐴 𝑦 < ( 𝐵 + 1 ) ) )
88 85 87 imbi12d ( 𝑥 = ( 𝐵 + 1 ) → ( ( 𝐵 < 𝑥 → ∃ 𝑦𝐴 𝑦 < 𝑥 ) ↔ ( 𝐵 < ( 𝐵 + 1 ) → ∃ 𝑦𝐴 𝑦 < ( 𝐵 + 1 ) ) ) )
89 88 rspcva ( ( ( 𝐵 + 1 ) ∈ ℝ ∧ ∀ 𝑥 ∈ ℝ ( 𝐵 < 𝑥 → ∃ 𝑦𝐴 𝑦 < 𝑥 ) ) → ( 𝐵 < ( 𝐵 + 1 ) → ∃ 𝑦𝐴 𝑦 < ( 𝐵 + 1 ) ) )
90 83 84 89 sylc ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) → ∃ 𝑦𝐴 𝑦 < ( 𝐵 + 1 ) )
91 nfv 𝑦 𝐵 < 𝑥
92 2 41 91 nf3an 𝑦 ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 )
93 nfv 𝑦 ¬ 𝐵 = -∞
94 92 93 nfan 𝑦 ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ )
95 43 3ad2antl1 ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ 𝑦𝐴 ) → 𝑦 ∈ ℝ* )
96 95 ad4ant13 ( ( ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) ∧ 𝑦𝐴 ) ∧ 𝑦 < ( 𝐵 + 1 ) ) → 𝑦 ∈ ℝ* )
97 80 adantr ( ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) ∧ 𝑦𝐴 ) → ( 𝐵 + 1 ) ∈ ℝ )
98 97 rexrd ( ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) ∧ 𝑦𝐴 ) → ( 𝐵 + 1 ) ∈ ℝ* )
99 98 adantr ( ( ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) ∧ 𝑦𝐴 ) ∧ 𝑦 < ( 𝐵 + 1 ) ) → ( 𝐵 + 1 ) ∈ ℝ* )
100 50 3adant3 ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) → 𝑥 ∈ ℝ* )
101 100 ad3antrrr ( ( ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) ∧ 𝑦𝐴 ) ∧ 𝑦 < ( 𝐵 + 1 ) ) → 𝑥 ∈ ℝ* )
102 simpr ( ( ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) ∧ 𝑦𝐴 ) ∧ 𝑦 < ( 𝐵 + 1 ) ) → 𝑦 < ( 𝐵 + 1 ) )
103 80 ltpnfd ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) → ( 𝐵 + 1 ) < +∞ )
104 56 adantr ( ( 𝑥 = +∞ ∧ ¬ 𝐵 = -∞ ) → +∞ = 𝑥 )
105 104 3ad2antl2 ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) → +∞ = 𝑥 )
106 103 105 breqtrd ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) → ( 𝐵 + 1 ) < 𝑥 )
107 106 ad2antrr ( ( ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) ∧ 𝑦𝐴 ) ∧ 𝑦 < ( 𝐵 + 1 ) ) → ( 𝐵 + 1 ) < 𝑥 )
108 96 99 101 102 107 xrlttrd ( ( ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) ∧ 𝑦𝐴 ) ∧ 𝑦 < ( 𝐵 + 1 ) ) → 𝑦 < 𝑥 )
109 108 ex ( ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) ∧ 𝑦𝐴 ) → ( 𝑦 < ( 𝐵 + 1 ) → 𝑦 < 𝑥 ) )
110 109 ex ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) → ( 𝑦𝐴 → ( 𝑦 < ( 𝐵 + 1 ) → 𝑦 < 𝑥 ) ) )
111 94 110 reximdai ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) → ( ∃ 𝑦𝐴 𝑦 < ( 𝐵 + 1 ) → ∃ 𝑦𝐴 𝑦 < 𝑥 ) )
112 90 111 mpd ( ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) ∧ ¬ 𝐵 = -∞ ) → ∃ 𝑦𝐴 𝑦 < 𝑥 )
113 66 112 pm2.61dan ( ( 𝜑𝑥 = +∞ ∧ 𝐵 < 𝑥 ) → ∃ 𝑦𝐴 𝑦 < 𝑥 )
114 9 23 24 113 syl3anc ( ( ( ( 𝜑𝑥 ∈ ℝ* ) ∧ ¬ 𝑥 ∈ ℝ ) ∧ 𝐵 < 𝑥 ) → ∃ 𝑦𝐴 𝑦 < 𝑥 )
115 114 ex ( ( ( 𝜑𝑥 ∈ ℝ* ) ∧ ¬ 𝑥 ∈ ℝ ) → ( 𝐵 < 𝑥 → ∃ 𝑦𝐴 𝑦 < 𝑥 ) )
116 8 115 pm2.61dan ( ( 𝜑𝑥 ∈ ℝ* ) → ( 𝐵 < 𝑥 → ∃ 𝑦𝐴 𝑦 < 𝑥 ) )
117 116 ex ( 𝜑 → ( 𝑥 ∈ ℝ* → ( 𝐵 < 𝑥 → ∃ 𝑦𝐴 𝑦 < 𝑥 ) ) )
118 1 117 ralrimi ( 𝜑 → ∀ 𝑥 ∈ ℝ* ( 𝐵 < 𝑥 → ∃ 𝑦𝐴 𝑦 < 𝑥 ) )
119 xrltso < Or ℝ*
120 119 a1i ( ⊤ → < Or ℝ* )
121 120 eqinf ( ⊤ → ( ( 𝐵 ∈ ℝ* ∧ ∀ 𝑥𝐴 ¬ 𝑥 < 𝐵 ∧ ∀ 𝑥 ∈ ℝ* ( 𝐵 < 𝑥 → ∃ 𝑦𝐴 𝑦 < 𝑥 ) ) → inf ( 𝐴 , ℝ* , < ) = 𝐵 ) )
122 121 mptru ( ( 𝐵 ∈ ℝ* ∧ ∀ 𝑥𝐴 ¬ 𝑥 < 𝐵 ∧ ∀ 𝑥 ∈ ℝ* ( 𝐵 < 𝑥 → ∃ 𝑦𝐴 𝑦 < 𝑥 ) ) → inf ( 𝐴 , ℝ* , < ) = 𝐵 )
123 4 5 118 122 syl3anc ( 𝜑 → inf ( 𝐴 , ℝ* , < ) = 𝐵 )