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

Metamath Proof Explorer

Theorem infleinf

Description: If any element of B can be approximated from above by members of A , then the infimum of A is less than or equal to the infimum of B . (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses infleinf.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )
infleinf.b ⊢ ( 𝜑 → 𝐵 ⊆ ℝ* )
infleinf.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ 𝐴 𝑧 ≤ ( 𝑥 +𝑒 𝑦 ) )
Assertion infleinf ( 𝜑 → inf ( 𝐴 , ℝ* , < ) ≤ inf ( 𝐵 , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 infleinf.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )
2 infleinf.b ⊢ ( 𝜑 → 𝐵 ⊆ ℝ* )
3 infleinf.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ 𝐴 𝑧 ≤ ( 𝑥 +𝑒 𝑦 ) )
4 infxrcl ⊢ ( 𝐴 ⊆ ℝ* → inf ( 𝐴 , ℝ* , < ) ∈ ℝ* )
5 1 4 syl ⊢ ( 𝜑 → inf ( 𝐴 , ℝ* , < ) ∈ ℝ* )
6 pnfge ⊢ ( inf ( 𝐴 , ℝ* , < ) ∈ ℝ* → inf ( 𝐴 , ℝ* , < ) ≤ +∞ )
7 5 6 syl ⊢ ( 𝜑 → inf ( 𝐴 , ℝ* , < ) ≤ +∞ )
8 7 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = ∅ ) → inf ( 𝐴 , ℝ* , < ) ≤ +∞ )
9 infeq1 ⊢ ( 𝐵 = ∅ → inf ( 𝐵 , ℝ* , < ) = inf ( ∅ , ℝ* , < ) )
10 xrinf0 ⊢ inf ( ∅ , ℝ* , < ) = +∞
11 10 a1i ⊢ ( 𝐵 = ∅ → inf ( ∅ , ℝ* , < ) = +∞ )
12 9 11 eqtrd ⊢ ( 𝐵 = ∅ → inf ( 𝐵 , ℝ* , < ) = +∞ )
13 12 eqcomd ⊢ ( 𝐵 = ∅ → +∞ = inf ( 𝐵 , ℝ* , < ) )
14 13 adantl ⊢ ( ( 𝜑 ∧ 𝐵 = ∅ ) → +∞ = inf ( 𝐵 , ℝ* , < ) )
15 8 14 breqtrd ⊢ ( ( 𝜑 ∧ 𝐵 = ∅ ) → inf ( 𝐴 , ℝ* , < ) ≤ inf ( 𝐵 , ℝ* , < ) )
16 neqne ⊢ ( ¬ 𝐵 = ∅ → 𝐵 ≠ ∅ )
17 16 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = ∅ ) → 𝐵 ≠ ∅ )
18 5 adantr ⊢ ( ( 𝜑 ∧ inf ( 𝐵 , ℝ* , < ) = -∞ ) → inf ( 𝐴 , ℝ* , < ) ∈ ℝ* )
19 id ⊢ ( 𝑟 ∈ ℝ → 𝑟 ∈ ℝ )
20 2re ⊢ 2 ∈ ℝ
21 20 a1i ⊢ ( 𝑟 ∈ ℝ → 2 ∈ ℝ )
22 19 21 resubcld ⊢ ( 𝑟 ∈ ℝ → ( 𝑟 − 2 ) ∈ ℝ )
23 22 adantl ⊢ ( ( ( 𝜑 ∧ inf ( 𝐵 , ℝ* , < ) = -∞ ) ∧ 𝑟 ∈ ℝ ) → ( 𝑟 − 2 ) ∈ ℝ )
24 simpr ⊢ ( ( 𝜑 ∧ inf ( 𝐵 , ℝ* , < ) = -∞ ) → inf ( 𝐵 , ℝ* , < ) = -∞ )
25 infxrunb2 ⊢ ( 𝐵 ⊆ ℝ* → ( ∀ 𝑦 ∈ ℝ ∃ 𝑥 ∈ 𝐵 𝑥 < 𝑦 ↔ inf ( 𝐵 , ℝ* , < ) = -∞ ) )
26 2 25 syl ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ℝ ∃ 𝑥 ∈ 𝐵 𝑥 < 𝑦 ↔ inf ( 𝐵 , ℝ* , < ) = -∞ ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ inf ( 𝐵 , ℝ* , < ) = -∞ ) → ( ∀ 𝑦 ∈ ℝ ∃ 𝑥 ∈ 𝐵 𝑥 < 𝑦 ↔ inf ( 𝐵 , ℝ* , < ) = -∞ ) )
28 24 27 mpbird ⊢ ( ( 𝜑 ∧ inf ( 𝐵 , ℝ* , < ) = -∞ ) → ∀ 𝑦 ∈ ℝ ∃ 𝑥 ∈ 𝐵 𝑥 < 𝑦 )
29 28 adantr ⊢ ( ( ( 𝜑 ∧ inf ( 𝐵 , ℝ* , < ) = -∞ ) ∧ 𝑟 ∈ ℝ ) → ∀ 𝑦 ∈ ℝ ∃ 𝑥 ∈ 𝐵 𝑥 < 𝑦 )
30 breq2 ⊢ ( 𝑦 = ( 𝑟 − 2 ) → ( 𝑥 < 𝑦 ↔ 𝑥 < ( 𝑟 − 2 ) ) )
31 30 rexbidv ⊢ ( 𝑦 = ( 𝑟 − 2 ) → ( ∃ 𝑥 ∈ 𝐵 𝑥 < 𝑦 ↔ ∃ 𝑥 ∈ 𝐵 𝑥 < ( 𝑟 − 2 ) ) )
32 31 rspcva ⊢ ( ( ( 𝑟 − 2 ) ∈ ℝ ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑥 ∈ 𝐵 𝑥 < 𝑦 ) → ∃ 𝑥 ∈ 𝐵 𝑥 < ( 𝑟 − 2 ) )
33 23 29 32 syl2anc ⊢ ( ( ( 𝜑 ∧ inf ( 𝐵 , ℝ* , < ) = -∞ ) ∧ 𝑟 ∈ ℝ ) → ∃ 𝑥 ∈ 𝐵 𝑥 < ( 𝑟 − 2 ) )
34 simpl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝜑 )
35 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
36 1rp ⊢ 1 ∈ ℝ+
37 36 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 1 ∈ ℝ+ )
38 1ex ⊢ 1 ∈ V
39 eleq1 ⊢ ( 𝑦 = 1 → ( 𝑦 ∈ ℝ+ ↔ 1 ∈ ℝ+ ) )
40 39 3anbi3d ⊢ ( 𝑦 = 1 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ℝ+ ) ↔ ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 1 ∈ ℝ+ ) ) )
41 oveq2 ⊢ ( 𝑦 = 1 → ( 𝑥 +𝑒 𝑦 ) = ( 𝑥 +𝑒 1 ) )
42 41 breq2d ⊢ ( 𝑦 = 1 → ( 𝑧 ≤ ( 𝑥 +𝑒 𝑦 ) ↔ 𝑧 ≤ ( 𝑥 +𝑒 1 ) ) )
43 42 rexbidv ⊢ ( 𝑦 = 1 → ( ∃ 𝑧 ∈ 𝐴 𝑧 ≤ ( 𝑥 +𝑒 𝑦 ) ↔ ∃ 𝑧 ∈ 𝐴 𝑧 ≤ ( 𝑥 +𝑒 1 ) ) )
44 40 43 imbi12d ⊢ ( 𝑦 = 1 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ 𝐴 𝑧 ≤ ( 𝑥 +𝑒 𝑦 ) ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 1 ∈ ℝ+ ) → ∃ 𝑧 ∈ 𝐴 𝑧 ≤ ( 𝑥 +𝑒 1 ) ) ) )
45 38 44 3 vtocl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 1 ∈ ℝ+ ) → ∃ 𝑧 ∈ 𝐴 𝑧 ≤ ( 𝑥 +𝑒 1 ) )
46 34 35 37 45 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑧 ∈ 𝐴 𝑧 ≤ ( 𝑥 +𝑒 1 ) )
47 46 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑧 ∈ 𝐴 𝑧 ≤ ( 𝑥 +𝑒 1 ) )
48 47 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < ( 𝑟 − 2 ) ) → ∃ 𝑧 ∈ 𝐴 𝑧 ≤ ( 𝑥 +𝑒 1 ) )
49 simp1l ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < ( 𝑟 − 2 ) ) → 𝜑 )
50 49 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < ( 𝑟 − 2 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≤ ( 𝑥 +𝑒 1 ) ) → 𝜑 )
51 50 1 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < ( 𝑟 − 2 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≤ ( 𝑥 +𝑒 1 ) ) → 𝐴 ⊆ ℝ* )
52 50 2 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < ( 𝑟 − 2 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≤ ( 𝑥 +𝑒 1 ) ) → 𝐵 ⊆ ℝ* )
53 simp1r ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < ( 𝑟 − 2 ) ) → 𝑟 ∈ ℝ )
54 53 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < ( 𝑟 − 2 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≤ ( 𝑥 +𝑒 1 ) ) → 𝑟 ∈ ℝ )
55 simp2 ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < ( 𝑟 − 2 ) ) → 𝑥 ∈ 𝐵 )
56 55 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < ( 𝑟 − 2 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≤ ( 𝑥 +𝑒 1 ) ) → 𝑥 ∈ 𝐵 )
57 simpll3 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < ( 𝑟 − 2 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≤ ( 𝑥 +𝑒 1 ) ) → 𝑥 < ( 𝑟 − 2 ) )
58 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < ( 𝑟 − 2 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≤ ( 𝑥 +𝑒 1 ) ) → 𝑧 ∈ 𝐴 )
59 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < ( 𝑟 − 2 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≤ ( 𝑥 +𝑒 1 ) ) → 𝑧 ≤ ( 𝑥 +𝑒 1 ) )
60 51 52 54 56 57 58 59 infleinflem2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < ( 𝑟 − 2 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≤ ( 𝑥 +𝑒 1 ) ) → 𝑧 < 𝑟 )
61 60 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < ( 𝑟 − 2 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 ≤ ( 𝑥 +𝑒 1 ) → 𝑧 < 𝑟 ) )
62 61 reximdva ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < ( 𝑟 − 2 ) ) → ( ∃ 𝑧 ∈ 𝐴 𝑧 ≤ ( 𝑥 +𝑒 1 ) → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑟 ) )
63 48 62 mpd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < ( 𝑟 − 2 ) ) → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑟 )
64 63 3exp ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) → ( 𝑥 ∈ 𝐵 → ( 𝑥 < ( 𝑟 − 2 ) → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑟 ) ) )
65 64 adantlr ⊢ ( ( ( 𝜑 ∧ inf ( 𝐵 , ℝ* , < ) = -∞ ) ∧ 𝑟 ∈ ℝ ) → ( 𝑥 ∈ 𝐵 → ( 𝑥 < ( 𝑟 − 2 ) → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑟 ) ) )
66 65 rexlimdv ⊢ ( ( ( 𝜑 ∧ inf ( 𝐵 , ℝ* , < ) = -∞ ) ∧ 𝑟 ∈ ℝ ) → ( ∃ 𝑥 ∈ 𝐵 𝑥 < ( 𝑟 − 2 ) → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑟 ) )
67 33 66 mpd ⊢ ( ( ( 𝜑 ∧ inf ( 𝐵 , ℝ* , < ) = -∞ ) ∧ 𝑟 ∈ ℝ ) → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑟 )
68 67 ralrimiva ⊢ ( ( 𝜑 ∧ inf ( 𝐵 , ℝ* , < ) = -∞ ) → ∀ 𝑟 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑟 )
69 infxrunb2 ⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑟 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑟 ↔ inf ( 𝐴 , ℝ* , < ) = -∞ ) )
70 1 69 syl ⊢ ( 𝜑 → ( ∀ 𝑟 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑟 ↔ inf ( 𝐴 , ℝ* , < ) = -∞ ) )
71 70 adantr ⊢ ( ( 𝜑 ∧ inf ( 𝐵 , ℝ* , < ) = -∞ ) → ( ∀ 𝑟 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑟 ↔ inf ( 𝐴 , ℝ* , < ) = -∞ ) )
72 68 71 mpbid ⊢ ( ( 𝜑 ∧ inf ( 𝐵 , ℝ* , < ) = -∞ ) → inf ( 𝐴 , ℝ* , < ) = -∞ )
73 72 24 eqtr4d ⊢ ( ( 𝜑 ∧ inf ( 𝐵 , ℝ* , < ) = -∞ ) → inf ( 𝐴 , ℝ* , < ) = inf ( 𝐵 , ℝ* , < ) )
74 18 73 xreqled ⊢ ( ( 𝜑 ∧ inf ( 𝐵 , ℝ* , < ) = -∞ ) → inf ( 𝐴 , ℝ* , < ) ≤ inf ( 𝐵 , ℝ* , < ) )
75 74 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ inf ( 𝐵 , ℝ* , < ) = -∞ ) → inf ( 𝐴 , ℝ* , < ) ≤ inf ( 𝐵 , ℝ* , < ) )
76 mnfxr ⊢ -∞ ∈ ℝ*
77 76 a1i ⊢ ( 𝜑 → -∞ ∈ ℝ* )
78 77 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ ¬ inf ( 𝐵 , ℝ* , < ) = -∞ ) → -∞ ∈ ℝ* )
79 infxrcl ⊢ ( 𝐵 ⊆ ℝ* → inf ( 𝐵 , ℝ* , < ) ∈ ℝ* )
80 2 79 syl ⊢ ( 𝜑 → inf ( 𝐵 , ℝ* , < ) ∈ ℝ* )
81 80 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ ¬ inf ( 𝐵 , ℝ* , < ) = -∞ ) → inf ( 𝐵 , ℝ* , < ) ∈ ℝ* )
82 mnfle ⊢ ( inf ( 𝐵 , ℝ* , < ) ∈ ℝ* → -∞ ≤ inf ( 𝐵 , ℝ* , < ) )
83 81 82 syl ⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ ¬ inf ( 𝐵 , ℝ* , < ) = -∞ ) → -∞ ≤ inf ( 𝐵 , ℝ* , < ) )
84 neqne ⊢ ( ¬ inf ( 𝐵 , ℝ* , < ) = -∞ → inf ( 𝐵 , ℝ* , < ) ≠ -∞ )
85 84 necomd ⊢ ( ¬ inf ( 𝐵 , ℝ* , < ) = -∞ → -∞ ≠ inf ( 𝐵 , ℝ* , < ) )
86 85 adantl ⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ ¬ inf ( 𝐵 , ℝ* , < ) = -∞ ) → -∞ ≠ inf ( 𝐵 , ℝ* , < ) )
87 78 81 83 86 xrleneltd ⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ ¬ inf ( 𝐵 , ℝ* , < ) = -∞ ) → -∞ < inf ( 𝐵 , ℝ* , < ) )
88 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ -∞ < inf ( 𝐵 , ℝ* , < ) ) → inf ( 𝐴 , ℝ* , < ) ∈ ℝ* )
89 80 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ -∞ < inf ( 𝐵 , ℝ* , < ) ) → inf ( 𝐵 , ℝ* , < ) ∈ ℝ* )
90 nfv ⊢ Ⅎ 𝑏 ( ( ( 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ -∞ < inf ( 𝐵 , ℝ* , < ) ) ∧ 𝑤 ∈ ℝ+ )
91 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ -∞ < inf ( 𝐵 , ℝ* , < ) ) ∧ 𝑤 ∈ ℝ+ ) → 𝐵 ⊆ ℝ* )
92 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ -∞ < inf ( 𝐵 , ℝ* , < ) ) ∧ 𝑤 ∈ ℝ+ ) → 𝐵 ≠ ∅ )
93 simpr ⊢ ( ( 𝜑 ∧ -∞ < inf ( 𝐵 , ℝ* , < ) ) → -∞ < inf ( 𝐵 , ℝ* , < ) )
94 infxrbnd2 ⊢ ( 𝐵 ⊆ ℝ* → ( ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝐵 𝑏 ≤ 𝑥 ↔ -∞ < inf ( 𝐵 , ℝ* , < ) ) )
95 2 94 syl ⊢ ( 𝜑 → ( ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝐵 𝑏 ≤ 𝑥 ↔ -∞ < inf ( 𝐵 , ℝ* , < ) ) )
96 95 adantr ⊢ ( ( 𝜑 ∧ -∞ < inf ( 𝐵 , ℝ* , < ) ) → ( ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝐵 𝑏 ≤ 𝑥 ↔ -∞ < inf ( 𝐵 , ℝ* , < ) ) )
97 93 96 mpbird ⊢ ( ( 𝜑 ∧ -∞ < inf ( 𝐵 , ℝ* , < ) ) → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝐵 𝑏 ≤ 𝑥 )
98 97 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ -∞ < inf ( 𝐵 , ℝ* , < ) ) ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝐵 𝑏 ≤ 𝑥 )
99 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ -∞ < inf ( 𝐵 , ℝ* , < ) ) ∧ 𝑤 ∈ ℝ+ ) → 𝑤 ∈ ℝ+ )
100 99 rphalfcld ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ -∞ < inf ( 𝐵 , ℝ* , < ) ) ∧ 𝑤 ∈ ℝ+ ) → ( 𝑤 / 2 ) ∈ ℝ+ )
101 90 91 92 98 100 infrpge ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ -∞ < inf ( 𝐵 , ℝ* , < ) ) ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑥 ∈ 𝐵 𝑥 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑤 / 2 ) ) )
102 simpll ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐵 ) → 𝜑 )
103 simpr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
104 rphalfcl ⊢ ( 𝑤 ∈ ℝ+ → ( 𝑤 / 2 ) ∈ ℝ+ )
105 104 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑤 / 2 ) ∈ ℝ+ )
106 ovex ⊢ ( 𝑤 / 2 ) ∈ V
107 eleq1 ⊢ ( 𝑦 = ( 𝑤 / 2 ) → ( 𝑦 ∈ ℝ+ ↔ ( 𝑤 / 2 ) ∈ ℝ+ ) )
108 107 3anbi3d ⊢ ( 𝑦 = ( 𝑤 / 2 ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ℝ+ ) ↔ ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 𝑤 / 2 ) ∈ ℝ+ ) ) )
109 oveq2 ⊢ ( 𝑦 = ( 𝑤 / 2 ) → ( 𝑥 +𝑒 𝑦 ) = ( 𝑥 +𝑒 ( 𝑤 / 2 ) ) )
110 109 breq2d ⊢ ( 𝑦 = ( 𝑤 / 2 ) → ( 𝑧 ≤ ( 𝑥 +𝑒 𝑦 ) ↔ 𝑧 ≤ ( 𝑥 +𝑒 ( 𝑤 / 2 ) ) ) )
111 110 rexbidv ⊢ ( 𝑦 = ( 𝑤 / 2 ) → ( ∃ 𝑧 ∈ 𝐴 𝑧 ≤ ( 𝑥 +𝑒 𝑦 ) ↔ ∃ 𝑧 ∈ 𝐴 𝑧 ≤ ( 𝑥 +𝑒 ( 𝑤 / 2 ) ) ) )
112 108 111 imbi12d ⊢ ( 𝑦 = ( 𝑤 / 2 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ 𝐴 𝑧 ≤ ( 𝑥 +𝑒 𝑦 ) ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 𝑤 / 2 ) ∈ ℝ+ ) → ∃ 𝑧 ∈ 𝐴 𝑧 ≤ ( 𝑥 +𝑒 ( 𝑤 / 2 ) ) ) ) )
113 106 112 3 vtocl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 𝑤 / 2 ) ∈ ℝ+ ) → ∃ 𝑧 ∈ 𝐴 𝑧 ≤ ( 𝑥 +𝑒 ( 𝑤 / 2 ) ) )
114 102 103 105 113 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑧 ∈ 𝐴 𝑧 ≤ ( 𝑥 +𝑒 ( 𝑤 / 2 ) ) )
115 114 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑤 / 2 ) ) ) → ∃ 𝑧 ∈ 𝐴 𝑧 ≤ ( 𝑥 +𝑒 ( 𝑤 / 2 ) ) )
116 simp11l ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑤 / 2 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 ≤ ( 𝑥 +𝑒 ( 𝑤 / 2 ) ) ) → 𝜑 )
117 116 1 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑤 / 2 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 ≤ ( 𝑥 +𝑒 ( 𝑤 / 2 ) ) ) → 𝐴 ⊆ ℝ* )
118 116 2 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑤 / 2 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 ≤ ( 𝑥 +𝑒 ( 𝑤 / 2 ) ) ) → 𝐵 ⊆ ℝ* )
119 simp11 ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑤 / 2 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 ≤ ( 𝑥 +𝑒 ( 𝑤 / 2 ) ) ) → ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) )
120 119 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑤 / 2 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 ≤ ( 𝑥 +𝑒 ( 𝑤 / 2 ) ) ) → 𝑤 ∈ ℝ+ )
121 simp12 ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑤 / 2 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 ≤ ( 𝑥 +𝑒 ( 𝑤 / 2 ) ) ) → 𝑥 ∈ 𝐵 )
122 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑤 / 2 ) ) ) → 𝑥 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑤 / 2 ) ) )
123 122 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑤 / 2 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 ≤ ( 𝑥 +𝑒 ( 𝑤 / 2 ) ) ) → 𝑥 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑤 / 2 ) ) )
124 simp2 ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑤 / 2 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 ≤ ( 𝑥 +𝑒 ( 𝑤 / 2 ) ) ) → 𝑧 ∈ 𝐴 )
125 simp3 ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑤 / 2 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 ≤ ( 𝑥 +𝑒 ( 𝑤 / 2 ) ) ) → 𝑧 ≤ ( 𝑥 +𝑒 ( 𝑤 / 2 ) ) )
126 117 118 120 121 123 124 125 infleinflem1 ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑤 / 2 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 ≤ ( 𝑥 +𝑒 ( 𝑤 / 2 ) ) ) → inf ( 𝐴 , ℝ* , < ) ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 𝑤 ) )
127 126 3exp ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑤 / 2 ) ) ) → ( 𝑧 ∈ 𝐴 → ( 𝑧 ≤ ( 𝑥 +𝑒 ( 𝑤 / 2 ) ) → inf ( 𝐴 , ℝ* , < ) ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 𝑤 ) ) ) )
128 127 rexlimdv ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑤 / 2 ) ) ) → ( ∃ 𝑧 ∈ 𝐴 𝑧 ≤ ( 𝑥 +𝑒 ( 𝑤 / 2 ) ) → inf ( 𝐴 , ℝ* , < ) ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 𝑤 ) ) )
129 115 128 mpd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑤 / 2 ) ) ) → inf ( 𝐴 , ℝ* , < ) ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 𝑤 ) )
130 129 3exp ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ( 𝑥 ∈ 𝐵 → ( 𝑥 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑤 / 2 ) ) → inf ( 𝐴 , ℝ* , < ) ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 𝑤 ) ) ) )
131 130 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ( ∃ 𝑥 ∈ 𝐵 𝑥 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑤 / 2 ) ) → inf ( 𝐴 , ℝ* , < ) ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 𝑤 ) ) )
132 131 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ -∞ < inf ( 𝐵 , ℝ* , < ) ) ∧ 𝑤 ∈ ℝ+ ) → ( ∃ 𝑥 ∈ 𝐵 𝑥 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑤 / 2 ) ) → inf ( 𝐴 , ℝ* , < ) ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 𝑤 ) ) )
133 101 132 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ -∞ < inf ( 𝐵 , ℝ* , < ) ) ∧ 𝑤 ∈ ℝ+ ) → inf ( 𝐴 , ℝ* , < ) ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 𝑤 ) )
134 88 89 133 xrlexaddrp ⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ -∞ < inf ( 𝐵 , ℝ* , < ) ) → inf ( 𝐴 , ℝ* , < ) ≤ inf ( 𝐵 , ℝ* , < ) )
135 87 134 syldan ⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ ¬ inf ( 𝐵 , ℝ* , < ) = -∞ ) → inf ( 𝐴 , ℝ* , < ) ≤ inf ( 𝐵 , ℝ* , < ) )
136 75 135 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ∅ ) → inf ( 𝐴 , ℝ* , < ) ≤ inf ( 𝐵 , ℝ* , < ) )
137 17 136 syldan ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = ∅ ) → inf ( 𝐴 , ℝ* , < ) ≤ inf ( 𝐵 , ℝ* , < ) )
138 15 137 pm2.61dan ⊢ ( 𝜑 → inf ( 𝐴 , ℝ* , < ) ≤ inf ( 𝐵 , ℝ* , < ) )