Metamath Proof Explorer


Theorem infrpgernmpt

Description: The infimum of a nonempty, bounded below, indexed subset of extended reals can be approximated from above by an element of the set. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses infrpgernmpt.x 𝑥 𝜑
infrpgernmpt.a ( 𝜑𝐴 ≠ ∅ )
infrpgernmpt.b ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ* )
infrpgernmpt.y ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 𝑦𝐵 )
infrpgernmpt.c ( 𝜑𝐶 ∈ ℝ+ )
Assertion infrpgernmpt ( 𝜑 → ∃ 𝑥𝐴 𝐵 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) )

Proof

Step Hyp Ref Expression
1 infrpgernmpt.x 𝑥 𝜑
2 infrpgernmpt.a ( 𝜑𝐴 ≠ ∅ )
3 infrpgernmpt.b ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ* )
4 infrpgernmpt.y ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 𝑦𝐵 )
5 infrpgernmpt.c ( 𝜑𝐶 ∈ ℝ+ )
6 nfv 𝑤 𝜑
7 eqid ( 𝑥𝐴𝐵 ) = ( 𝑥𝐴𝐵 )
8 1 7 3 rnmptssd ( 𝜑 → ran ( 𝑥𝐴𝐵 ) ⊆ ℝ* )
9 1 3 7 2 rnmptn0 ( 𝜑 → ran ( 𝑥𝐴𝐵 ) ≠ ∅ )
10 breq1 ( 𝑦 = 𝑤 → ( 𝑦𝐵𝑤𝐵 ) )
11 10 ralbidv ( 𝑦 = 𝑤 → ( ∀ 𝑥𝐴 𝑦𝐵 ↔ ∀ 𝑥𝐴 𝑤𝐵 ) )
12 11 cbvrexvw ( ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 𝑦𝐵 ↔ ∃ 𝑤 ∈ ℝ ∀ 𝑥𝐴 𝑤𝐵 )
13 4 12 sylib ( 𝜑 → ∃ 𝑤 ∈ ℝ ∀ 𝑥𝐴 𝑤𝐵 )
14 13 rnmptlb ( 𝜑 → ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥𝐴𝐵 ) 𝑤𝑧 )
15 6 8 9 14 5 infrpge ( 𝜑 → ∃ 𝑤 ∈ ran ( 𝑥𝐴𝐵 ) 𝑤 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) )
16 simpll ( ( ( 𝜑𝑤 ∈ ran ( 𝑥𝐴𝐵 ) ) ∧ 𝑤 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) → 𝜑 )
17 simpr ( ( ( 𝜑𝑤 ∈ ran ( 𝑥𝐴𝐵 ) ) ∧ 𝑤 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) → 𝑤 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) )
18 vex 𝑤 ∈ V
19 7 elrnmpt ( 𝑤 ∈ V → ( 𝑤 ∈ ran ( 𝑥𝐴𝐵 ) ↔ ∃ 𝑥𝐴 𝑤 = 𝐵 ) )
20 18 19 ax-mp ( 𝑤 ∈ ran ( 𝑥𝐴𝐵 ) ↔ ∃ 𝑥𝐴 𝑤 = 𝐵 )
21 20 biimpi ( 𝑤 ∈ ran ( 𝑥𝐴𝐵 ) → ∃ 𝑥𝐴 𝑤 = 𝐵 )
22 21 ad2antlr ( ( ( 𝜑𝑤 ∈ ran ( 𝑥𝐴𝐵 ) ) ∧ 𝑤 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) → ∃ 𝑥𝐴 𝑤 = 𝐵 )
23 nfcv 𝑥 𝑤
24 nfcv 𝑥
25 nfmpt1 𝑥 ( 𝑥𝐴𝐵 )
26 25 nfrn 𝑥 ran ( 𝑥𝐴𝐵 )
27 nfcv 𝑥*
28 nfcv 𝑥 <
29 26 27 28 nfinf 𝑥 inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < )
30 nfcv 𝑥 +𝑒
31 nfcv 𝑥 𝐶
32 29 30 31 nfov 𝑥 ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 )
33 23 24 32 nfbr 𝑥 𝑤 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 )
34 1 33 nfan 𝑥 ( 𝜑𝑤 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) )
35 id ( 𝑤 = 𝐵𝑤 = 𝐵 )
36 35 eqcomd ( 𝑤 = 𝐵𝐵 = 𝑤 )
37 36 adantl ( ( 𝑤 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ∧ 𝑤 = 𝐵 ) → 𝐵 = 𝑤 )
38 simpl ( ( 𝑤 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ∧ 𝑤 = 𝐵 ) → 𝑤 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) )
39 37 38 eqbrtrd ( ( 𝑤 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ∧ 𝑤 = 𝐵 ) → 𝐵 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) )
40 39 ex ( 𝑤 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) → ( 𝑤 = 𝐵𝐵 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) )
41 40 a1d ( 𝑤 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) → ( 𝑥𝐴 → ( 𝑤 = 𝐵𝐵 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) ) )
42 41 adantl ( ( 𝜑𝑤 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) → ( 𝑥𝐴 → ( 𝑤 = 𝐵𝐵 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) ) )
43 34 42 reximdai ( ( 𝜑𝑤 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) → ( ∃ 𝑥𝐴 𝑤 = 𝐵 → ∃ 𝑥𝐴 𝐵 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) )
44 43 imp ( ( ( 𝜑𝑤 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) ∧ ∃ 𝑥𝐴 𝑤 = 𝐵 ) → ∃ 𝑥𝐴 𝐵 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) )
45 16 17 22 44 syl21anc ( ( ( 𝜑𝑤 ∈ ran ( 𝑥𝐴𝐵 ) ) ∧ 𝑤 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) → ∃ 𝑥𝐴 𝐵 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) )
46 45 rexlimdva2 ( 𝜑 → ( ∃ 𝑤 ∈ ran ( 𝑥𝐴𝐵 ) 𝑤 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) → ∃ 𝑥𝐴 𝐵 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) )
47 15 46 mpd ( 𝜑 → ∃ 𝑥𝐴 𝐵 ≤ ( inf ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) )