This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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