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 ⊢ Ⅎ x φ
infrpgernmpt.a ⊢ φ → A ≠ ∅
infrpgernmpt.b ⊢ φ ∧ x ∈ A → B ∈ ℝ *
infrpgernmpt.y ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A y ≤ B
infrpgernmpt.c ⊢ φ → C ∈ ℝ +
Assertion infrpgernmpt ⊢ φ → ∃ x ∈ A B ≤ inf ran ⁡ x ∈ A ⟼ B ℝ * < + 𝑒 C

Proof

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