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 ( 𝐴 , ℝ* , < ) = 𝐵 )