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

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 ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) )