Metamath Proof Explorer


Theorem supxrgere

Description: If a real number can be approximated from below by members of a set, then it is less than or equal to the supremum of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses supxrgere.xph 𝑥 𝜑
supxrgere.a ( 𝜑𝐴 ⊆ ℝ* )
supxrgere.b ( 𝜑𝐵 ∈ ℝ )
supxrgere.y ( ( 𝜑𝑥 ∈ ℝ+ ) → ∃ 𝑦𝐴 ( 𝐵𝑥 ) < 𝑦 )
Assertion supxrgere ( 𝜑𝐵 ≤ sup ( 𝐴 , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 supxrgere.xph 𝑥 𝜑
2 supxrgere.a ( 𝜑𝐴 ⊆ ℝ* )
3 supxrgere.b ( 𝜑𝐵 ∈ ℝ )
4 supxrgere.y ( ( 𝜑𝑥 ∈ ℝ+ ) → ∃ 𝑦𝐴 ( 𝐵𝑥 ) < 𝑦 )
5 rexr ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
6 pnfxr +∞ ∈ ℝ*
7 6 a1i ( 𝐵 ∈ ℝ → +∞ ∈ ℝ* )
8 ltpnf ( 𝐵 ∈ ℝ → 𝐵 < +∞ )
9 5 7 8 xrltled ( 𝐵 ∈ ℝ → 𝐵 ≤ +∞ )
10 3 9 syl ( 𝜑𝐵 ≤ +∞ )
11 10 adantr ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) → 𝐵 ≤ +∞ )
12 id ( sup ( 𝐴 , ℝ* , < ) = +∞ → sup ( 𝐴 , ℝ* , < ) = +∞ )
13 12 eqcomd ( sup ( 𝐴 , ℝ* , < ) = +∞ → +∞ = sup ( 𝐴 , ℝ* , < ) )
14 13 adantl ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) → +∞ = sup ( 𝐴 , ℝ* , < ) )
15 11 14 breqtrd ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) → 𝐵 ≤ sup ( 𝐴 , ℝ* , < ) )
16 simpl ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) → 𝜑 )
17 1rp 1 ∈ ℝ+
18 nfcv 𝑥 1
19 nfv 𝑥 1 ∈ ℝ+
20 1 19 nfan 𝑥 ( 𝜑 ∧ 1 ∈ ℝ+ )
21 nfv 𝑥𝑦𝐴 ( 𝐵 − 1 ) < 𝑦
22 20 21 nfim 𝑥 ( ( 𝜑 ∧ 1 ∈ ℝ+ ) → ∃ 𝑦𝐴 ( 𝐵 − 1 ) < 𝑦 )
23 eleq1 ( 𝑥 = 1 → ( 𝑥 ∈ ℝ+ ↔ 1 ∈ ℝ+ ) )
24 23 anbi2d ( 𝑥 = 1 → ( ( 𝜑𝑥 ∈ ℝ+ ) ↔ ( 𝜑 ∧ 1 ∈ ℝ+ ) ) )
25 oveq2 ( 𝑥 = 1 → ( 𝐵𝑥 ) = ( 𝐵 − 1 ) )
26 25 breq1d ( 𝑥 = 1 → ( ( 𝐵𝑥 ) < 𝑦 ↔ ( 𝐵 − 1 ) < 𝑦 ) )
27 26 rexbidv ( 𝑥 = 1 → ( ∃ 𝑦𝐴 ( 𝐵𝑥 ) < 𝑦 ↔ ∃ 𝑦𝐴 ( 𝐵 − 1 ) < 𝑦 ) )
28 24 27 imbi12d ( 𝑥 = 1 → ( ( ( 𝜑𝑥 ∈ ℝ+ ) → ∃ 𝑦𝐴 ( 𝐵𝑥 ) < 𝑦 ) ↔ ( ( 𝜑 ∧ 1 ∈ ℝ+ ) → ∃ 𝑦𝐴 ( 𝐵 − 1 ) < 𝑦 ) ) )
29 18 22 28 4 vtoclgf ( 1 ∈ ℝ+ → ( ( 𝜑 ∧ 1 ∈ ℝ+ ) → ∃ 𝑦𝐴 ( 𝐵 − 1 ) < 𝑦 ) )
30 17 29 ax-mp ( ( 𝜑 ∧ 1 ∈ ℝ+ ) → ∃ 𝑦𝐴 ( 𝐵 − 1 ) < 𝑦 )
31 17 30 mpan2 ( 𝜑 → ∃ 𝑦𝐴 ( 𝐵 − 1 ) < 𝑦 )
32 31 adantr ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) → ∃ 𝑦𝐴 ( 𝐵 − 1 ) < 𝑦 )
33 mnfxr -∞ ∈ ℝ*
34 33 a1i ( ( 𝜑𝑦𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) → -∞ ∈ ℝ* )
35 2 sselda ( ( 𝜑𝑦𝐴 ) → 𝑦 ∈ ℝ* )
36 35 3adant3 ( ( 𝜑𝑦𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) → 𝑦 ∈ ℝ* )
37 supxrcl ( 𝐴 ⊆ ℝ* → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
38 2 37 syl ( 𝜑 → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
39 38 3ad2ant1 ( ( 𝜑𝑦𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
40 peano2rem ( 𝐵 ∈ ℝ → ( 𝐵 − 1 ) ∈ ℝ )
41 3 40 syl ( 𝜑 → ( 𝐵 − 1 ) ∈ ℝ )
42 41 rexrd ( 𝜑 → ( 𝐵 − 1 ) ∈ ℝ* )
43 42 adantr ( ( 𝜑 ∧ ¬ -∞ < 𝑦 ) → ( 𝐵 − 1 ) ∈ ℝ* )
44 43 3ad2antl1 ( ( ( 𝜑𝑦𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) ∧ ¬ -∞ < 𝑦 ) → ( 𝐵 − 1 ) ∈ ℝ* )
45 36 adantr ( ( ( 𝜑𝑦𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) ∧ ¬ -∞ < 𝑦 ) → 𝑦 ∈ ℝ* )
46 33 a1i ( ( ( 𝜑𝑦𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) ∧ ¬ -∞ < 𝑦 ) → -∞ ∈ ℝ* )
47 simpl3 ( ( ( 𝜑𝑦𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) ∧ ¬ -∞ < 𝑦 ) → ( 𝐵 − 1 ) < 𝑦 )
48 simpr ( ( ( 𝜑𝑦𝐴 ) ∧ ¬ -∞ < 𝑦 ) → ¬ -∞ < 𝑦 )
49 35 adantr ( ( ( 𝜑𝑦𝐴 ) ∧ ¬ -∞ < 𝑦 ) → 𝑦 ∈ ℝ* )
50 33 a1i ( ( ( 𝜑𝑦𝐴 ) ∧ ¬ -∞ < 𝑦 ) → -∞ ∈ ℝ* )
51 xrlenlt ( ( 𝑦 ∈ ℝ* ∧ -∞ ∈ ℝ* ) → ( 𝑦 ≤ -∞ ↔ ¬ -∞ < 𝑦 ) )
52 49 50 51 syl2anc ( ( ( 𝜑𝑦𝐴 ) ∧ ¬ -∞ < 𝑦 ) → ( 𝑦 ≤ -∞ ↔ ¬ -∞ < 𝑦 ) )
53 48 52 mpbird ( ( ( 𝜑𝑦𝐴 ) ∧ ¬ -∞ < 𝑦 ) → 𝑦 ≤ -∞ )
54 53 3adantl3 ( ( ( 𝜑𝑦𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) ∧ ¬ -∞ < 𝑦 ) → 𝑦 ≤ -∞ )
55 44 45 46 47 54 xrltletrd ( ( ( 𝜑𝑦𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) ∧ ¬ -∞ < 𝑦 ) → ( 𝐵 − 1 ) < -∞ )
56 nltmnf ( ( 𝐵 − 1 ) ∈ ℝ* → ¬ ( 𝐵 − 1 ) < -∞ )
57 42 56 syl ( 𝜑 → ¬ ( 𝐵 − 1 ) < -∞ )
58 57 adantr ( ( 𝜑 ∧ ¬ -∞ < 𝑦 ) → ¬ ( 𝐵 − 1 ) < -∞ )
59 58 3ad2antl1 ( ( ( 𝜑𝑦𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) ∧ ¬ -∞ < 𝑦 ) → ¬ ( 𝐵 − 1 ) < -∞ )
60 55 59 condan ( ( 𝜑𝑦𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) → -∞ < 𝑦 )
61 2 adantr ( ( 𝜑𝑦𝐴 ) → 𝐴 ⊆ ℝ* )
62 simpr ( ( 𝜑𝑦𝐴 ) → 𝑦𝐴 )
63 supxrub ( ( 𝐴 ⊆ ℝ*𝑦𝐴 ) → 𝑦 ≤ sup ( 𝐴 , ℝ* , < ) )
64 61 62 63 syl2anc ( ( 𝜑𝑦𝐴 ) → 𝑦 ≤ sup ( 𝐴 , ℝ* , < ) )
65 64 3adant3 ( ( 𝜑𝑦𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) → 𝑦 ≤ sup ( 𝐴 , ℝ* , < ) )
66 34 36 39 60 65 xrltletrd ( ( 𝜑𝑦𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) → -∞ < sup ( 𝐴 , ℝ* , < ) )
67 66 3exp ( 𝜑 → ( 𝑦𝐴 → ( ( 𝐵 − 1 ) < 𝑦 → -∞ < sup ( 𝐴 , ℝ* , < ) ) ) )
68 67 adantr ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) → ( 𝑦𝐴 → ( ( 𝐵 − 1 ) < 𝑦 → -∞ < sup ( 𝐴 , ℝ* , < ) ) ) )
69 68 rexlimdv ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) → ( ∃ 𝑦𝐴 ( 𝐵 − 1 ) < 𝑦 → -∞ < sup ( 𝐴 , ℝ* , < ) ) )
70 32 69 mpd ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) → -∞ < sup ( 𝐴 , ℝ* , < ) )
71 simpr ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) → ¬ sup ( 𝐴 , ℝ* , < ) = +∞ )
72 nltpnft ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* → ( sup ( 𝐴 , ℝ* , < ) = +∞ ↔ ¬ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
73 38 72 syl ( 𝜑 → ( sup ( 𝐴 , ℝ* , < ) = +∞ ↔ ¬ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
74 73 adantr ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) → ( sup ( 𝐴 , ℝ* , < ) = +∞ ↔ ¬ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
75 71 74 mtbid ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) → ¬ ¬ sup ( 𝐴 , ℝ* , < ) < +∞ )
76 75 notnotrd ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) → sup ( 𝐴 , ℝ* , < ) < +∞ )
77 70 76 jca ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) → ( -∞ < sup ( 𝐴 , ℝ* , < ) ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
78 38 adantr ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
79 xrrebnd ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* → ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ↔ ( -∞ < sup ( 𝐴 , ℝ* , < ) ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) ) )
80 78 79 syl ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) → ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ↔ ( -∞ < sup ( 𝐴 , ℝ* , < ) ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) ) )
81 77 80 mpbird ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ )
82 simpl ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ ¬ 𝐵 ≤ sup ( 𝐴 , ℝ* , < ) ) → ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) )
83 simpr ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ ¬ 𝐵 ≤ sup ( 𝐴 , ℝ* , < ) ) → ¬ 𝐵 ≤ sup ( 𝐴 , ℝ* , < ) )
84 82 simprd ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ ¬ 𝐵 ≤ sup ( 𝐴 , ℝ* , < ) ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ )
85 3 ad2antrr ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ ¬ 𝐵 ≤ sup ( 𝐴 , ℝ* , < ) ) → 𝐵 ∈ ℝ )
86 84 85 ltnled ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ ¬ 𝐵 ≤ sup ( 𝐴 , ℝ* , < ) ) → ( sup ( 𝐴 , ℝ* , < ) < 𝐵 ↔ ¬ 𝐵 ≤ sup ( 𝐴 , ℝ* , < ) ) )
87 83 86 mpbird ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ ¬ 𝐵 ≤ sup ( 𝐴 , ℝ* , < ) ) → sup ( 𝐴 , ℝ* , < ) < 𝐵 )
88 simpll ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐵 ) → 𝜑 )
89 3 adantr ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) → 𝐵 ∈ ℝ )
90 simpr ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ )
91 89 90 resubcld ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) → ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ )
92 91 adantr ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐵 ) → ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ )
93 simpr ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐵 ) → sup ( 𝐴 , ℝ* , < ) < 𝐵 )
94 90 adantr ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐵 ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ )
95 88 3 syl ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐵 ) → 𝐵 ∈ ℝ )
96 94 95 posdifd ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐵 ) → ( sup ( 𝐴 , ℝ* , < ) < 𝐵 ↔ 0 < ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ) )
97 93 96 mpbid ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐵 ) → 0 < ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) )
98 92 97 elrpd ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐵 ) → ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ+ )
99 ovex ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ∈ V
100 nfcv 𝑥 ( 𝐵 − sup ( 𝐴 , ℝ* , < ) )
101 nfv 𝑥 ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ+
102 1 101 nfan 𝑥 ( 𝜑 ∧ ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ+ )
103 nfv 𝑥𝑦𝐴 ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ) < 𝑦
104 102 103 nfim 𝑥 ( ( 𝜑 ∧ ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ+ ) → ∃ 𝑦𝐴 ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ) < 𝑦 )
105 eleq1 ( 𝑥 = ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) → ( 𝑥 ∈ ℝ+ ↔ ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ+ ) )
106 105 anbi2d ( 𝑥 = ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) → ( ( 𝜑𝑥 ∈ ℝ+ ) ↔ ( 𝜑 ∧ ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ+ ) ) )
107 oveq2 ( 𝑥 = ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) → ( 𝐵𝑥 ) = ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ) )
108 107 breq1d ( 𝑥 = ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) → ( ( 𝐵𝑥 ) < 𝑦 ↔ ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ) < 𝑦 ) )
109 108 rexbidv ( 𝑥 = ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) → ( ∃ 𝑦𝐴 ( 𝐵𝑥 ) < 𝑦 ↔ ∃ 𝑦𝐴 ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ) < 𝑦 ) )
110 106 109 imbi12d ( 𝑥 = ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) → ( ( ( 𝜑𝑥 ∈ ℝ+ ) → ∃ 𝑦𝐴 ( 𝐵𝑥 ) < 𝑦 ) ↔ ( ( 𝜑 ∧ ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ+ ) → ∃ 𝑦𝐴 ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ) < 𝑦 ) ) )
111 100 104 110 4 vtoclgf ( ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ∈ V → ( ( 𝜑 ∧ ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ+ ) → ∃ 𝑦𝐴 ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ) < 𝑦 ) )
112 99 111 ax-mp ( ( 𝜑 ∧ ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ+ ) → ∃ 𝑦𝐴 ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ) < 𝑦 )
113 88 98 112 syl2anc ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐵 ) → ∃ 𝑦𝐴 ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ) < 𝑦 )
114 3 recnd ( 𝜑𝐵 ∈ ℂ )
115 114 ad3antrrr ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐵 ) ∧ ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ) < 𝑦 ) → 𝐵 ∈ ℂ )
116 90 recnd ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) → sup ( 𝐴 , ℝ* , < ) ∈ ℂ )
117 116 ad2antrr ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐵 ) ∧ ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ) < 𝑦 ) → sup ( 𝐴 , ℝ* , < ) ∈ ℂ )
118 115 117 nncand ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐵 ) ∧ ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ) < 𝑦 ) → ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ) = sup ( 𝐴 , ℝ* , < ) )
119 118 eqcomd ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐵 ) ∧ ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ) < 𝑦 ) → sup ( 𝐴 , ℝ* , < ) = ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ) )
120 simpr ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐵 ) ∧ ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ) < 𝑦 ) → ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ) < 𝑦 )
121 119 120 eqbrtrd ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐵 ) ∧ ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ) < 𝑦 ) → sup ( 𝐴 , ℝ* , < ) < 𝑦 )
122 121 ex ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐵 ) → ( ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ) < 𝑦 → sup ( 𝐴 , ℝ* , < ) < 𝑦 ) )
123 122 adantr ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐵 ) ∧ 𝑦𝐴 ) → ( ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ) < 𝑦 → sup ( 𝐴 , ℝ* , < ) < 𝑦 ) )
124 123 reximdva ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐵 ) → ( ∃ 𝑦𝐴 ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ* , < ) ) ) < 𝑦 → ∃ 𝑦𝐴 sup ( 𝐴 , ℝ* , < ) < 𝑦 ) )
125 113 124 mpd ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐵 ) → ∃ 𝑦𝐴 sup ( 𝐴 , ℝ* , < ) < 𝑦 )
126 82 87 125 syl2anc ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ ¬ 𝐵 ≤ sup ( 𝐴 , ℝ* , < ) ) → ∃ 𝑦𝐴 sup ( 𝐴 , ℝ* , < ) < 𝑦 )
127 61 37 syl ( ( 𝜑𝑦𝐴 ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
128 35 127 xrlenltd ( ( 𝜑𝑦𝐴 ) → ( 𝑦 ≤ sup ( 𝐴 , ℝ* , < ) ↔ ¬ sup ( 𝐴 , ℝ* , < ) < 𝑦 ) )
129 64 128 mpbid ( ( 𝜑𝑦𝐴 ) → ¬ sup ( 𝐴 , ℝ* , < ) < 𝑦 )
130 129 ralrimiva ( 𝜑 → ∀ 𝑦𝐴 ¬ sup ( 𝐴 , ℝ* , < ) < 𝑦 )
131 ralnex ( ∀ 𝑦𝐴 ¬ sup ( 𝐴 , ℝ* , < ) < 𝑦 ↔ ¬ ∃ 𝑦𝐴 sup ( 𝐴 , ℝ* , < ) < 𝑦 )
132 130 131 sylib ( 𝜑 → ¬ ∃ 𝑦𝐴 sup ( 𝐴 , ℝ* , < ) < 𝑦 )
133 132 ad2antrr ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ ¬ 𝐵 ≤ sup ( 𝐴 , ℝ* , < ) ) → ¬ ∃ 𝑦𝐴 sup ( 𝐴 , ℝ* , < ) < 𝑦 )
134 126 133 condan ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) → 𝐵 ≤ sup ( 𝐴 , ℝ* , < ) )
135 16 81 134 syl2anc ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) → 𝐵 ≤ sup ( 𝐴 , ℝ* , < ) )
136 15 135 pm2.61dan ( 𝜑𝐵 ≤ sup ( 𝐴 , ℝ* , < ) )