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 ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) ≤ 𝐷 )