Metamath Proof Explorer

Theorem infxrunb3rnmpt

Description: The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses infxrunb3rnmpt.1 ⊢ Ⅎ x φ
infxrunb3rnmpt.2 ⊢ Ⅎ y φ
infxrunb3rnmpt.3 ⊢ φ ∧ x ∈ A → B ∈ ℝ *
Assertion infxrunb3rnmpt ⊢ φ → ∀ y ∈ ℝ ∃ x ∈ A B ≤ y ↔ inf ran ⁡ x ∈ A ⟼ B ℝ * < = −∞

Proof

Step Hyp Ref Expression
1 infxrunb3rnmpt.1 ⊢ Ⅎ x φ
2 infxrunb3rnmpt.2 ⊢ Ⅎ y φ
3 infxrunb3rnmpt.3 ⊢ φ ∧ x ∈ A → B ∈ ℝ *
4 nfmpt1 ⊢ Ⅎ _ x x ∈ A ⟼ B
5 4 nfrn ⊢ Ⅎ _ x ran ⁡ x ∈ A ⟼ B
6 nfv ⊢ Ⅎ x z ≤ y
7 5 6 nfrexw ⊢ Ⅎ x ∃ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
8 simpr ⊢ φ ∧ x ∈ A → x ∈ A
9 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
10 9 elrnmpt1 ⊢ x ∈ A ∧ B ∈ ℝ * → B ∈ ran ⁡ x ∈ A ⟼ B
11 8 3 10 syl2anc ⊢ φ ∧ x ∈ A → B ∈ ran ⁡ x ∈ A ⟼ B
12 11 3adant3 ⊢ φ ∧ x ∈ A ∧ B ≤ y → B ∈ ran ⁡ x ∈ A ⟼ B
13 simp3 ⊢ φ ∧ x ∈ A ∧ B ≤ y → B ≤ y
14 breq1 ⊢ z = B → z ≤ y ↔ B ≤ y
15 14 rspcev ⊢ B ∈ ran ⁡ x ∈ A ⟼ B ∧ B ≤ y → ∃ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
16 12 13 15 syl2anc ⊢ φ ∧ x ∈ A ∧ B ≤ y → ∃ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
17 16 3exp ⊢ φ → x ∈ A → B ≤ y → ∃ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
18 1 7 17 rexlimd ⊢ φ → ∃ x ∈ A B ≤ y → ∃ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
19 nfv ⊢ Ⅎ z ∃ x ∈ A B ≤ y
20 vex ⊢ z ∈ V
21 9 elrnmpt ⊢ z ∈ V → z ∈ ran ⁡ x ∈ A ⟼ B ↔ ∃ x ∈ A z = B
22 20 21 ax-mp ⊢ z ∈ ran ⁡ x ∈ A ⟼ B ↔ ∃ x ∈ A z = B
23 22 biimpi ⊢ z ∈ ran ⁡ x ∈ A ⟼ B → ∃ x ∈ A z = B
24 14 biimpcd ⊢ z ≤ y → z = B → B ≤ y
25 24 a1d ⊢ z ≤ y → x ∈ A → z = B → B ≤ y
26 6 25 reximdai ⊢ z ≤ y → ∃ x ∈ A z = B → ∃ x ∈ A B ≤ y
27 26 com12 ⊢ ∃ x ∈ A z = B → z ≤ y → ∃ x ∈ A B ≤ y
28 23 27 syl ⊢ z ∈ ran ⁡ x ∈ A ⟼ B → z ≤ y → ∃ x ∈ A B ≤ y
29 19 28 rexlimi ⊢ ∃ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y → ∃ x ∈ A B ≤ y
30 29 a1i ⊢ φ → ∃ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y → ∃ x ∈ A B ≤ y
31 18 30 impbid ⊢ φ → ∃ x ∈ A B ≤ y ↔ ∃ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
32 2 31 ralbid ⊢ φ → ∀ y ∈ ℝ ∃ x ∈ A B ≤ y ↔ ∀ y ∈ ℝ ∃ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
33 1 9 3 rnmptssd ⊢ φ → ran ⁡ x ∈ A ⟼ B ⊆ ℝ *
34 infxrunb3 ⊢ ran ⁡ x ∈ A ⟼ B ⊆ ℝ * → ∀ y ∈ ℝ ∃ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y ↔ inf ran ⁡ x ∈ A ⟼ B ℝ * < = −∞
35 33 34 syl ⊢ φ → ∀ y ∈ ℝ ∃ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y ↔ inf ran ⁡ x ∈ A ⟼ B ℝ * < = −∞
36 32 35 bitrd ⊢ φ → ∀ y ∈ ℝ ∃ x ∈ A B ≤ y ↔ inf ran ⁡ x ∈ A ⟼ B ℝ * < = −∞