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

Metamath Proof Explorer

Theorem infxrlbrnmpt2

Description: A member of a nonempty indexed set of reals is greater than or equal to the set's lower bound. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses infxrlbrnmpt2.x ⊢ Ⅎ 𝑥 𝜑
infxrlbrnmpt2.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
infxrlbrnmpt2.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
infxrlbrnmpt2.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ* )
infxrlbrnmpt2.e ⊢ ( 𝑥 = 𝐶 → 𝐵 = 𝐷 )
Assertion infxrlbrnmpt2 ( 𝜑 → inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) ≤ 𝐷 )

Proof

Step Hyp Ref Expression
1 infxrlbrnmpt2.x ⊢ Ⅎ 𝑥 𝜑
2 infxrlbrnmpt2.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
3 infxrlbrnmpt2.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
4 infxrlbrnmpt2.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ* )
5 infxrlbrnmpt2.e ⊢ ( 𝑥 = 𝐶 → 𝐵 = 𝐷 )
6 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
7 1 6 2 rnmptssd ⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ* )
8 6 5 elrnmpt1s ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ ℝ* ) → 𝐷 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
9 3 4 8 syl2anc ⊢ ( 𝜑 → 𝐷 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
10 infxrlb ⊢ ( ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ* ∧ 𝐷 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) ≤ 𝐷 )
11 7 9 10 syl2anc ⊢ ( 𝜑 → inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) ≤ 𝐷 )