Theorem infxrrefi

Description: The real and extended real infima match when the set is finite. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Assertion	infxrrefi	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → inf ( 𝐴 , ℝ* , < ) = inf ( 𝐴 , ℝ , < ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → 𝐴 ⊆ ℝ )
2		simp3	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → 𝐴 ≠ ∅ )
3		fiminre2	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )
4	3	3adant3	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )
5		infxrre	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → inf ( 𝐴 , ℝ* , < ) = inf ( 𝐴 , ℝ , < ) )
6	1 2 4 5	syl3anc	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → inf ( 𝐴 , ℝ* , < ) = inf ( 𝐴 , ℝ , < ) )