Metamath Proof Explorer

Theorem supxrgelem

Description: If an extended 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 supxrgelem.xph ⊒ β„² π‘₯ πœ‘
supxrgelem.a ⊒ ( πœ‘ β†’ 𝐴 βŠ† ℝ* )
supxrgelem.b ⊒ ( πœ‘ β†’ 𝐡 ∈ ℝ* )
supxrgelem.y ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 π‘₯ ) )
Assertion supxrgelem ( πœ‘ β†’ 𝐡 ≀ sup ( 𝐴 , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 supxrgelem.xph ⊒ β„² π‘₯ πœ‘
2 supxrgelem.a ⊒ ( πœ‘ β†’ 𝐴 βŠ† ℝ* )
3 supxrgelem.b ⊒ ( πœ‘ β†’ 𝐡 ∈ ℝ* )
4 supxrgelem.y ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 π‘₯ ) )
5 pnfge ⊒ ( 𝐡 ∈ ℝ* β†’ 𝐡 ≀ +∞ )
6 3 5 syl ⊒ ( πœ‘ β†’ 𝐡 ≀ +∞ )
7 6 adantr ⊒ ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) β†’ 𝐡 ≀ +∞ )
8 id ⊒ ( sup ( 𝐴 , ℝ* , < ) = +∞ β†’ sup ( 𝐴 , ℝ* , < ) = +∞ )
9 8 eqcomd ⊒ ( sup ( 𝐴 , ℝ* , < ) = +∞ β†’ +∞ = sup ( 𝐴 , ℝ* , < ) )
10 9 adantl ⊒ ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) β†’ +∞ = sup ( 𝐴 , ℝ* , < ) )
11 7 10 breqtrd ⊒ ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) β†’ 𝐡 ≀ sup ( 𝐴 , ℝ* , < ) )
12 simpl ⊒ ( ( πœ‘ ∧ Β¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) β†’ πœ‘ )
13 1rp ⊒ 1 ∈ ℝ+
14 nfcv ⊒ β„² π‘₯ 1
15 nfv ⊒ β„² π‘₯ 1 ∈ ℝ+
16 1 15 nfan ⊒ β„² π‘₯ ( πœ‘ ∧ 1 ∈ ℝ+ )
17 nfv ⊒ β„² π‘₯ βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 1 )
18 16 17 nfim ⊒ β„² π‘₯ ( ( πœ‘ ∧ 1 ∈ ℝ+ ) β†’ βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 1 ) )
19 eleq1 ⊒ ( π‘₯ = 1 β†’ ( π‘₯ ∈ ℝ+ ↔ 1 ∈ ℝ+ ) )
20 19 anbi2d ⊒ ( π‘₯ = 1 β†’ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ↔ ( πœ‘ ∧ 1 ∈ ℝ+ ) ) )
21 oveq2 ⊒ ( π‘₯ = 1 β†’ ( 𝑦 +𝑒 π‘₯ ) = ( 𝑦 +𝑒 1 ) )
22 21 breq2d ⊒ ( π‘₯ = 1 β†’ ( 𝐡 < ( 𝑦 +𝑒 π‘₯ ) ↔ 𝐡 < ( 𝑦 +𝑒 1 ) ) )
23 22 rexbidv ⊒ ( π‘₯ = 1 β†’ ( βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 π‘₯ ) ↔ βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 1 ) ) )
24 20 23 imbi12d ⊒ ( π‘₯ = 1 β†’ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 π‘₯ ) ) ↔ ( ( πœ‘ ∧ 1 ∈ ℝ+ ) β†’ βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 1 ) ) ) )
25 14 18 24 4 vtoclgf ⊒ ( 1 ∈ ℝ+ β†’ ( ( πœ‘ ∧ 1 ∈ ℝ+ ) β†’ βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 1 ) ) )
26 13 25 ax-mp ⊒ ( ( πœ‘ ∧ 1 ∈ ℝ+ ) β†’ βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 1 ) )
27 13 26 mpan2 ⊒ ( πœ‘ β†’ βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 1 ) )
28 27 adantr ⊒ ( ( πœ‘ ∧ Β¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) β†’ βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 1 ) )
29 mnfxr ⊒ -∞ ∈ ℝ*
30 29 a1i ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ∧ 𝐡 < ( 𝑦 +𝑒 1 ) ) β†’ -∞ ∈ ℝ* )
31 2 sselda ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ) β†’ 𝑦 ∈ ℝ* )
32 31 3adant3 ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ∧ 𝐡 < ( 𝑦 +𝑒 1 ) ) β†’ 𝑦 ∈ ℝ* )
33 supxrcl ⊒ ( 𝐴 βŠ† ℝ* β†’ sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
34 2 33 syl ⊒ ( πœ‘ β†’ sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
35 34 3ad2ant1 ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ∧ 𝐡 < ( 𝑦 +𝑒 1 ) ) β†’ sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
36 simpl3 ⊒ ( ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ∧ 𝐡 < ( 𝑦 +𝑒 1 ) ) ∧ Β¬ -∞ < 𝑦 ) β†’ 𝐡 < ( 𝑦 +𝑒 1 ) )
37 simpr ⊒ ( ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ) ∧ Β¬ -∞ < 𝑦 ) β†’ Β¬ -∞ < 𝑦 )
38 31 adantr ⊒ ( ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ) ∧ Β¬ -∞ < 𝑦 ) β†’ 𝑦 ∈ ℝ* )
39 ngtmnft ⊒ ( 𝑦 ∈ ℝ* β†’ ( 𝑦 = -∞ ↔ Β¬ -∞ < 𝑦 ) )
40 38 39 syl ⊒ ( ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ) ∧ Β¬ -∞ < 𝑦 ) β†’ ( 𝑦 = -∞ ↔ Β¬ -∞ < 𝑦 ) )
41 37 40 mpbird ⊒ ( ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ) ∧ Β¬ -∞ < 𝑦 ) β†’ 𝑦 = -∞ )
42 41 oveq1d ⊒ ( ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ) ∧ Β¬ -∞ < 𝑦 ) β†’ ( 𝑦 +𝑒 1 ) = ( -∞ +𝑒 1 ) )
43 1xr ⊒ 1 ∈ ℝ*
44 43 a1i ⊒ ( ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ) ∧ Β¬ -∞ < 𝑦 ) β†’ 1 ∈ ℝ* )
45 1re ⊒ 1 ∈ ℝ
46 renepnf ⊒ ( 1 ∈ ℝ β†’ 1 β‰  +∞ )
47 45 46 ax-mp ⊒ 1 β‰  +∞
48 47 a1i ⊒ ( ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ) ∧ Β¬ -∞ < 𝑦 ) β†’ 1 β‰  +∞ )
49 xaddmnf2 ⊒ ( ( 1 ∈ ℝ* ∧ 1 β‰  +∞ ) β†’ ( -∞ +𝑒 1 ) = -∞ )
50 44 48 49 syl2anc ⊒ ( ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ) ∧ Β¬ -∞ < 𝑦 ) β†’ ( -∞ +𝑒 1 ) = -∞ )
51 42 50 eqtrd ⊒ ( ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ) ∧ Β¬ -∞ < 𝑦 ) β†’ ( 𝑦 +𝑒 1 ) = -∞ )
52 51 3adantl3 ⊒ ( ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ∧ 𝐡 < ( 𝑦 +𝑒 1 ) ) ∧ Β¬ -∞ < 𝑦 ) β†’ ( 𝑦 +𝑒 1 ) = -∞ )
53 36 52 breqtrd ⊒ ( ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ∧ 𝐡 < ( 𝑦 +𝑒 1 ) ) ∧ Β¬ -∞ < 𝑦 ) β†’ 𝐡 < -∞ )
54 nltmnf ⊒ ( 𝐡 ∈ ℝ* β†’ Β¬ 𝐡 < -∞ )
55 3 54 syl ⊒ ( πœ‘ β†’ Β¬ 𝐡 < -∞ )
56 55 adantr ⊒ ( ( πœ‘ ∧ Β¬ -∞ < 𝑦 ) β†’ Β¬ 𝐡 < -∞ )
57 56 3ad2antl1 ⊒ ( ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ∧ 𝐡 < ( 𝑦 +𝑒 1 ) ) ∧ Β¬ -∞ < 𝑦 ) β†’ Β¬ 𝐡 < -∞ )
58 53 57 condan ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ∧ 𝐡 < ( 𝑦 +𝑒 1 ) ) β†’ -∞ < 𝑦 )
59 2 adantr ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ) β†’ 𝐴 βŠ† ℝ* )
60 simpr ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ) β†’ 𝑦 ∈ 𝐴 )
61 supxrub ⊒ ( ( 𝐴 βŠ† ℝ* ∧ 𝑦 ∈ 𝐴 ) β†’ 𝑦 ≀ sup ( 𝐴 , ℝ* , < ) )
62 59 60 61 syl2anc ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ) β†’ 𝑦 ≀ sup ( 𝐴 , ℝ* , < ) )
63 62 3adant3 ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ∧ 𝐡 < ( 𝑦 +𝑒 1 ) ) β†’ 𝑦 ≀ sup ( 𝐴 , ℝ* , < ) )
64 30 32 35 58 63 xrltletrd ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ∧ 𝐡 < ( 𝑦 +𝑒 1 ) ) β†’ -∞ < sup ( 𝐴 , ℝ* , < ) )
65 64 3exp ⊒ ( πœ‘ β†’ ( 𝑦 ∈ 𝐴 β†’ ( 𝐡 < ( 𝑦 +𝑒 1 ) β†’ -∞ < sup ( 𝐴 , ℝ* , < ) ) ) )
66 65 adantr ⊒ ( ( πœ‘ ∧ Β¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) β†’ ( 𝑦 ∈ 𝐴 β†’ ( 𝐡 < ( 𝑦 +𝑒 1 ) β†’ -∞ < sup ( 𝐴 , ℝ* , < ) ) ) )
67 66 rexlimdv ⊒ ( ( πœ‘ ∧ Β¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) β†’ ( βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 1 ) β†’ -∞ < sup ( 𝐴 , ℝ* , < ) ) )
68 28 67 mpd ⊒ ( ( πœ‘ ∧ Β¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) β†’ -∞ < sup ( 𝐴 , ℝ* , < ) )
69 simpr ⊒ ( ( πœ‘ ∧ Β¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) β†’ Β¬ sup ( 𝐴 , ℝ* , < ) = +∞ )
70 nltpnft ⊒ ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* β†’ ( sup ( 𝐴 , ℝ* , < ) = +∞ ↔ Β¬ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
71 34 70 syl ⊒ ( πœ‘ β†’ ( sup ( 𝐴 , ℝ* , < ) = +∞ ↔ Β¬ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
72 71 adantr ⊒ ( ( πœ‘ ∧ Β¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) β†’ ( sup ( 𝐴 , ℝ* , < ) = +∞ ↔ Β¬ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
73 69 72 mtbid ⊒ ( ( πœ‘ ∧ Β¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) β†’ Β¬ Β¬ sup ( 𝐴 , ℝ* , < ) < +∞ )
74 73 notnotrd ⊒ ( ( πœ‘ ∧ Β¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) β†’ sup ( 𝐴 , ℝ* , < ) < +∞ )
75 68 74 jca ⊒ ( ( πœ‘ ∧ Β¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) β†’ ( -∞ < sup ( 𝐴 , ℝ* , < ) ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
76 34 adantr ⊒ ( ( πœ‘ ∧ Β¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) β†’ sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
77 xrrebnd ⊒ ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* β†’ ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ↔ ( -∞ < sup ( 𝐴 , ℝ* , < ) ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) ) )
78 76 77 syl ⊒ ( ( πœ‘ ∧ Β¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) β†’ ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ↔ ( -∞ < sup ( 𝐴 , ℝ* , < ) ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) ) )
79 75 78 mpbird ⊒ ( ( πœ‘ ∧ Β¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) β†’ sup ( 𝐴 , ℝ* , < ) ∈ ℝ )
80 simpl ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ Β¬ 𝐡 ≀ sup ( 𝐴 , ℝ* , < ) ) β†’ ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) )
81 simpr ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ Β¬ 𝐡 ≀ sup ( 𝐴 , ℝ* , < ) ) β†’ Β¬ 𝐡 ≀ sup ( 𝐴 , ℝ* , < ) )
82 34 adantr ⊒ ( ( πœ‘ ∧ Β¬ 𝐡 ≀ sup ( 𝐴 , ℝ* , < ) ) β†’ sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
83 3 adantr ⊒ ( ( πœ‘ ∧ Β¬ 𝐡 ≀ sup ( 𝐴 , ℝ* , < ) ) β†’ 𝐡 ∈ ℝ* )
84 xrltnle ⊒ ( ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* ∧ 𝐡 ∈ ℝ* ) β†’ ( sup ( 𝐴 , ℝ* , < ) < 𝐡 ↔ Β¬ 𝐡 ≀ sup ( 𝐴 , ℝ* , < ) ) )
85 82 83 84 syl2anc ⊒ ( ( πœ‘ ∧ Β¬ 𝐡 ≀ sup ( 𝐴 , ℝ* , < ) ) β†’ ( sup ( 𝐴 , ℝ* , < ) < 𝐡 ↔ Β¬ 𝐡 ≀ sup ( 𝐴 , ℝ* , < ) ) )
86 85 adantlr ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ Β¬ 𝐡 ≀ sup ( 𝐴 , ℝ* , < ) ) β†’ ( sup ( 𝐴 , ℝ* , < ) < 𝐡 ↔ Β¬ 𝐡 ≀ sup ( 𝐴 , ℝ* , < ) ) )
87 81 86 mpbird ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ Β¬ 𝐡 ≀ sup ( 𝐴 , ℝ* , < ) ) β†’ sup ( 𝐴 , ℝ* , < ) < 𝐡 )
88 simpll ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ πœ‘ )
89 29 a1i ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ -∞ ∈ ℝ* )
90 88 34 syl ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
91 88 3 syl ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ 𝐡 ∈ ℝ* )
92 mnfle ⊒ ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* β†’ -∞ ≀ sup ( 𝐴 , ℝ* , < ) )
93 34 92 syl ⊒ ( πœ‘ β†’ -∞ ≀ sup ( 𝐴 , ℝ* , < ) )
94 93 ad2antrr ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ -∞ ≀ sup ( 𝐴 , ℝ* , < ) )
95 simpr ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ sup ( 𝐴 , ℝ* , < ) < 𝐡 )
96 89 90 91 94 95 xrlelttrd ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ -∞ < 𝐡 )
97 id ⊒ ( πœ‘ β†’ πœ‘ )
98 13 a1i ⊒ ( πœ‘ β†’ 1 ∈ ℝ+ )
99 97 98 26 syl2anc ⊒ ( πœ‘ β†’ βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 1 ) )
100 99 ad2antrr ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 1 ) )
101 3 3ad2ant1 ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ∧ 𝐡 < ( 𝑦 +𝑒 1 ) ) β†’ 𝐡 ∈ ℝ* )
102 43 a1i ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ∧ 𝐡 < ( 𝑦 +𝑒 1 ) ) β†’ 1 ∈ ℝ* )
103 32 102 jca ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ∧ 𝐡 < ( 𝑦 +𝑒 1 ) ) β†’ ( 𝑦 ∈ ℝ* ∧ 1 ∈ ℝ* ) )
104 xaddcl ⊒ ( ( 𝑦 ∈ ℝ* ∧ 1 ∈ ℝ* ) β†’ ( 𝑦 +𝑒 1 ) ∈ ℝ* )
105 103 104 syl ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ∧ 𝐡 < ( 𝑦 +𝑒 1 ) ) β†’ ( 𝑦 +𝑒 1 ) ∈ ℝ* )
106 pnfxr ⊒ +∞ ∈ ℝ*
107 106 a1i ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ∧ 𝐡 < ( 𝑦 +𝑒 1 ) ) β†’ +∞ ∈ ℝ* )
108 simp3 ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ∧ 𝐡 < ( 𝑦 +𝑒 1 ) ) β†’ 𝐡 < ( 𝑦 +𝑒 1 ) )
109 31 43 104 sylancl ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ) β†’ ( 𝑦 +𝑒 1 ) ∈ ℝ* )
110 pnfge ⊒ ( ( 𝑦 +𝑒 1 ) ∈ ℝ* β†’ ( 𝑦 +𝑒 1 ) ≀ +∞ )
111 109 110 syl ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ) β†’ ( 𝑦 +𝑒 1 ) ≀ +∞ )
112 111 3adant3 ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ∧ 𝐡 < ( 𝑦 +𝑒 1 ) ) β†’ ( 𝑦 +𝑒 1 ) ≀ +∞ )
113 101 105 107 108 112 xrltletrd ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ∧ 𝐡 < ( 𝑦 +𝑒 1 ) ) β†’ 𝐡 < +∞ )
114 113 3exp ⊒ ( πœ‘ β†’ ( 𝑦 ∈ 𝐴 β†’ ( 𝐡 < ( 𝑦 +𝑒 1 ) β†’ 𝐡 < +∞ ) ) )
115 114 rexlimdv ⊒ ( πœ‘ β†’ ( βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 1 ) β†’ 𝐡 < +∞ ) )
116 88 115 syl ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ ( βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 1 ) β†’ 𝐡 < +∞ ) )
117 100 116 mpd ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ 𝐡 < +∞ )
118 96 117 jca ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ ( -∞ < 𝐡 ∧ 𝐡 < +∞ ) )
119 xrrebnd ⊒ ( 𝐡 ∈ ℝ* β†’ ( 𝐡 ∈ ℝ ↔ ( -∞ < 𝐡 ∧ 𝐡 < +∞ ) ) )
120 91 119 syl ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ ( 𝐡 ∈ ℝ ↔ ( -∞ < 𝐡 ∧ 𝐡 < +∞ ) ) )
121 118 120 mpbird ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ 𝐡 ∈ ℝ )
122 simpr ⊒ ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) β†’ sup ( 𝐴 , ℝ* , < ) ∈ ℝ )
123 122 adantr ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ sup ( 𝐴 , ℝ* , < ) ∈ ℝ )
124 121 123 resubcld ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ )
125 27 115 mpd ⊒ ( πœ‘ β†’ 𝐡 < +∞ )
126 125 ad2antrr ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ 𝐡 < +∞ )
127 96 126 jca ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ ( -∞ < 𝐡 ∧ 𝐡 < +∞ ) )
128 127 120 mpbird ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ 𝐡 ∈ ℝ )
129 123 128 posdifd ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ ( sup ( 𝐴 , ℝ* , < ) < 𝐡 ↔ 0 < ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) )
130 95 129 mpbid ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ 0 < ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) )
131 124 130 elrpd ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ+ )
132 ovex ⊒ ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ∈ V
133 nfcv ⊒ β„² π‘₯ ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) )
134 nfv ⊒ β„² π‘₯ ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ+
135 1 134 nfan ⊒ β„² π‘₯ ( πœ‘ ∧ ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ+ )
136 nfv ⊒ β„² π‘₯ βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) )
137 135 136 nfim ⊒ β„² π‘₯ ( ( πœ‘ ∧ ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ+ ) β†’ βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) )
138 eleq1 ⊒ ( π‘₯ = ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) β†’ ( π‘₯ ∈ ℝ+ ↔ ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ+ ) )
139 138 anbi2d ⊒ ( π‘₯ = ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) β†’ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ↔ ( πœ‘ ∧ ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ+ ) ) )
140 oveq2 ⊒ ( π‘₯ = ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) β†’ ( 𝑦 +𝑒 π‘₯ ) = ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) )
141 140 breq2d ⊒ ( π‘₯ = ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) β†’ ( 𝐡 < ( 𝑦 +𝑒 π‘₯ ) ↔ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) )
142 141 rexbidv ⊒ ( π‘₯ = ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) β†’ ( βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 π‘₯ ) ↔ βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) )
143 139 142 imbi12d ⊒ ( π‘₯ = ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) β†’ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 π‘₯ ) ) ↔ ( ( πœ‘ ∧ ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ+ ) β†’ βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) ) )
144 133 137 143 4 vtoclgf ⊒ ( ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ∈ V β†’ ( ( πœ‘ ∧ ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ+ ) β†’ βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) )
145 132 144 ax-mp ⊒ ( ( πœ‘ ∧ ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ+ ) β†’ βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) )
146 88 131 145 syl2anc ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) )
147 ltpnf ⊒ ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ β†’ sup ( 𝐴 , ℝ* , < ) < +∞ )
148 147 adantr ⊒ ( ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ∧ 𝑦 = +∞ ) β†’ sup ( 𝐴 , ℝ* , < ) < +∞ )
149 id ⊒ ( 𝑦 = +∞ β†’ 𝑦 = +∞ )
150 149 eqcomd ⊒ ( 𝑦 = +∞ β†’ +∞ = 𝑦 )
151 150 adantl ⊒ ( ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ∧ 𝑦 = +∞ ) β†’ +∞ = 𝑦 )
152 148 151 breqtrd ⊒ ( ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ∧ 𝑦 = +∞ ) β†’ sup ( 𝐴 , ℝ* , < ) < 𝑦 )
153 152 adantll ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑦 = +∞ ) β†’ sup ( 𝐴 , ℝ* , < ) < 𝑦 )
154 153 ad5ant15 ⊒ ( ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) ∧ 𝑦 = +∞ ) β†’ sup ( 𝐴 , ℝ* , < ) < 𝑦 )
155 simplll ⊒ ( ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) ∧ Β¬ 𝑦 = +∞ ) β†’ ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) )
156 simpl ⊒ ( ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) ∧ Β¬ -∞ < 𝑦 ) β†’ ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) )
157 88 41 sylanl1 ⊒ ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ Β¬ -∞ < 𝑦 ) β†’ 𝑦 = -∞ )
158 157 adantlr ⊒ ( ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) ∧ Β¬ -∞ < 𝑦 ) β†’ 𝑦 = -∞ )
159 simplr ⊒ ( ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) ∧ 𝑦 = -∞ ) β†’ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) )
160 oveq1 ⊒ ( 𝑦 = -∞ β†’ ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) = ( -∞ +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) )
161 160 adantl ⊒ ( ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) ∧ 𝑦 = -∞ ) β†’ ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) = ( -∞ +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) )
162 128 123 resubcld ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ )
163 162 rexrd ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ* )
164 163 ad3antrrr ⊒ ( ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) ∧ 𝑦 = -∞ ) β†’ ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ* )
165 renepnf ⊒ ( ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ β†’ ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) β‰  +∞ )
166 124 165 syl ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) β‰  +∞ )
167 166 ad3antrrr ⊒ ( ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) ∧ 𝑦 = -∞ ) β†’ ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) β‰  +∞ )
168 xaddmnf2 ⊒ ( ( ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ* ∧ ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) β‰  +∞ ) β†’ ( -∞ +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) = -∞ )
169 164 167 168 syl2anc ⊒ ( ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) ∧ 𝑦 = -∞ ) β†’ ( -∞ +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) = -∞ )
170 161 169 eqtrd ⊒ ( ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) ∧ 𝑦 = -∞ ) β†’ ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) = -∞ )
171 159 170 breqtrd ⊒ ( ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) ∧ 𝑦 = -∞ ) β†’ 𝐡 < -∞ )
172 156 158 171 syl2anc ⊒ ( ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) ∧ Β¬ -∞ < 𝑦 ) β†’ 𝐡 < -∞ )
173 55 ad5antr ⊒ ( ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) ∧ Β¬ -∞ < 𝑦 ) β†’ Β¬ 𝐡 < -∞ )
174 172 173 condan ⊒ ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) β†’ -∞ < 𝑦 )
175 174 adantr ⊒ ( ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) ∧ Β¬ 𝑦 = +∞ ) β†’ -∞ < 𝑦 )
176 simp3 ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ∧ Β¬ 𝑦 = +∞ ) β†’ Β¬ 𝑦 = +∞ )
177 31 3adant3 ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ∧ Β¬ 𝑦 = +∞ ) β†’ 𝑦 ∈ ℝ* )
178 nltpnft ⊒ ( 𝑦 ∈ ℝ* β†’ ( 𝑦 = +∞ ↔ Β¬ 𝑦 < +∞ ) )
179 177 178 syl ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ∧ Β¬ 𝑦 = +∞ ) β†’ ( 𝑦 = +∞ ↔ Β¬ 𝑦 < +∞ ) )
180 176 179 mtbid ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ∧ Β¬ 𝑦 = +∞ ) β†’ Β¬ Β¬ 𝑦 < +∞ )
181 180 notnotrd ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ∧ Β¬ 𝑦 = +∞ ) β†’ 𝑦 < +∞ )
182 181 3adant1r ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ∧ Β¬ 𝑦 = +∞ ) β†’ 𝑦 < +∞ )
183 182 ad5ant135 ⊒ ( ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) ∧ Β¬ 𝑦 = +∞ ) β†’ 𝑦 < +∞ )
184 175 183 jca ⊒ ( ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) ∧ Β¬ 𝑦 = +∞ ) β†’ ( -∞ < 𝑦 ∧ 𝑦 < +∞ ) )
185 31 adantlr ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) β†’ 𝑦 ∈ ℝ* )
186 185 ad5ant13 ⊒ ( ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) ∧ Β¬ 𝑦 = +∞ ) β†’ 𝑦 ∈ ℝ* )
187 xrrebnd ⊒ ( 𝑦 ∈ ℝ* β†’ ( 𝑦 ∈ ℝ ↔ ( -∞ < 𝑦 ∧ 𝑦 < +∞ ) ) )
188 186 187 syl ⊒ ( ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) ∧ Β¬ 𝑦 = +∞ ) β†’ ( 𝑦 ∈ ℝ ↔ ( -∞ < 𝑦 ∧ 𝑦 < +∞ ) ) )
189 184 188 mpbird ⊒ ( ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) ∧ Β¬ 𝑦 = +∞ ) β†’ 𝑦 ∈ ℝ )
190 simplr ⊒ ( ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) ∧ Β¬ 𝑦 = +∞ ) β†’ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) )
191 121 ad2antrr ⊒ ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) β†’ 𝐡 ∈ ℝ )
192 simpr ⊒ ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) β†’ 𝑦 ∈ ℝ )
193 124 adantr ⊒ ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) β†’ ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ )
194 rexadd ⊒ ( ( 𝑦 ∈ ℝ ∧ ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ∈ ℝ ) β†’ ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) = ( 𝑦 + ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) )
195 192 193 194 syl2anc ⊒ ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) β†’ ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) = ( 𝑦 + ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) )
196 192 193 readdcld ⊒ ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) β†’ ( 𝑦 + ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ∈ ℝ )
197 195 196 eqeltrd ⊒ ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) β†’ ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ∈ ℝ )
198 197 adantr ⊒ ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) β†’ ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ∈ ℝ )
199 simpr ⊒ ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) β†’ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) )
200 191 198 191 199 ltsub1dd ⊒ ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) β†’ ( 𝐡 βˆ’ 𝐡 ) < ( ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) βˆ’ 𝐡 ) )
201 121 recnd ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ 𝐡 ∈ β„‚ )
202 201 subidd ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ ( 𝐡 βˆ’ 𝐡 ) = 0 )
203 202 ad2antrr ⊒ ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) β†’ ( 𝐡 βˆ’ 𝐡 ) = 0 )
204 201 adantr ⊒ ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) β†’ 𝐡 ∈ β„‚ )
205 192 recnd ⊒ ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) β†’ 𝑦 ∈ β„‚ )
206 122 recnd ⊒ ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) β†’ sup ( 𝐴 , ℝ* , < ) ∈ β„‚ )
207 206 ad2antrr ⊒ ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) β†’ sup ( 𝐴 , ℝ* , < ) ∈ β„‚ )
208 205 207 subcld ⊒ ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) β†’ ( 𝑦 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ∈ β„‚ )
209 205 204 207 addsub12d ⊒ ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) β†’ ( 𝑦 + ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) = ( 𝐡 + ( 𝑦 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) )
210 195 209 eqtrd ⊒ ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) β†’ ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) = ( 𝐡 + ( 𝑦 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) )
211 204 208 210 mvrladdd ⊒ ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) β†’ ( ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) βˆ’ 𝐡 ) = ( 𝑦 βˆ’ sup ( 𝐴 , ℝ* , < ) ) )
212 211 adantr ⊒ ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) β†’ ( ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) βˆ’ 𝐡 ) = ( 𝑦 βˆ’ sup ( 𝐴 , ℝ* , < ) ) )
213 203 212 breq12d ⊒ ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) β†’ ( ( 𝐡 βˆ’ 𝐡 ) < ( ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) βˆ’ 𝐡 ) ↔ 0 < ( 𝑦 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) )
214 200 213 mpbid ⊒ ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) β†’ 0 < ( 𝑦 βˆ’ sup ( 𝐴 , ℝ* , < ) ) )
215 123 ad2antrr ⊒ ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) β†’ sup ( 𝐴 , ℝ* , < ) ∈ ℝ )
216 simplr ⊒ ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) β†’ 𝑦 ∈ ℝ )
217 215 216 posdifd ⊒ ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) β†’ ( sup ( 𝐴 , ℝ* , < ) < 𝑦 ↔ 0 < ( 𝑦 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) )
218 214 217 mpbird ⊒ ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) β†’ sup ( 𝐴 , ℝ* , < ) < 𝑦 )
219 155 189 190 218 syl21anc ⊒ ( ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) ∧ Β¬ 𝑦 = +∞ ) β†’ sup ( 𝐴 , ℝ* , < ) < 𝑦 )
220 154 219 pm2.61dan ⊒ ( ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) ) β†’ sup ( 𝐴 , ℝ* , < ) < 𝑦 )
221 220 ex ⊒ ( ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) ∧ 𝑦 ∈ 𝐴 ) β†’ ( 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) β†’ sup ( 𝐴 , ℝ* , < ) < 𝑦 ) )
222 221 reximdva ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ ( βˆƒ 𝑦 ∈ 𝐴 𝐡 < ( 𝑦 +𝑒 ( 𝐡 βˆ’ sup ( 𝐴 , ℝ* , < ) ) ) β†’ βˆƒ 𝑦 ∈ 𝐴 sup ( 𝐴 , ℝ* , < ) < 𝑦 ) )
223 146 222 mpd ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) < 𝐡 ) β†’ βˆƒ 𝑦 ∈ 𝐴 sup ( 𝐴 , ℝ* , < ) < 𝑦 )
224 80 87 223 syl2anc ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ Β¬ 𝐡 ≀ sup ( 𝐴 , ℝ* , < ) ) β†’ βˆƒ 𝑦 ∈ 𝐴 sup ( 𝐴 , ℝ* , < ) < 𝑦 )
225 59 33 syl ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ) β†’ sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
226 31 225 xrlenltd ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ) β†’ ( 𝑦 ≀ sup ( 𝐴 , ℝ* , < ) ↔ Β¬ sup ( 𝐴 , ℝ* , < ) < 𝑦 ) )
227 62 226 mpbid ⊒ ( ( πœ‘ ∧ 𝑦 ∈ 𝐴 ) β†’ Β¬ sup ( 𝐴 , ℝ* , < ) < 𝑦 )
228 227 ralrimiva ⊒ ( πœ‘ β†’ βˆ€ 𝑦 ∈ 𝐴 Β¬ sup ( 𝐴 , ℝ* , < ) < 𝑦 )
229 ralnex ⊒ ( βˆ€ 𝑦 ∈ 𝐴 Β¬ sup ( 𝐴 , ℝ* , < ) < 𝑦 ↔ Β¬ βˆƒ 𝑦 ∈ 𝐴 sup ( 𝐴 , ℝ* , < ) < 𝑦 )
230 228 229 sylib ⊒ ( πœ‘ β†’ Β¬ βˆƒ 𝑦 ∈ 𝐴 sup ( 𝐴 , ℝ* , < ) < 𝑦 )
231 230 ad2antrr ⊒ ( ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ Β¬ 𝐡 ≀ sup ( 𝐴 , ℝ* , < ) ) β†’ Β¬ βˆƒ 𝑦 ∈ 𝐴 sup ( 𝐴 , ℝ* , < ) < 𝑦 )
232 224 231 condan ⊒ ( ( πœ‘ ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) β†’ 𝐡 ≀ sup ( 𝐴 , ℝ* , < ) )
233 12 79 232 syl2anc ⊒ ( ( πœ‘ ∧ Β¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) β†’ 𝐡 ≀ sup ( 𝐴 , ℝ* , < ) )
234 11 233 pm2.61dan ⊒ ( πœ‘ β†’ 𝐡 ≀ sup ( 𝐴 , ℝ* , < ) )