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

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 ⊢ Ⅎ 𝑥 𝜑
infxrunb3rnmpt.2 ⊢ Ⅎ 𝑦 𝜑
infxrunb3rnmpt.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
Assertion infxrunb3rnmpt ( 𝜑 → ( ∀ 𝑦 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) = -∞ ) )

Proof

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