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