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	$⊢ (A \subseteq ℝ \land A \in Fin \land A \neq \emptyset) \to inf (A ℝ^{*} <) = inf (A ℝ <)$

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \subseteq ℝ \land A \in Fin \land A \neq \emptyset) \to A \subseteq ℝ$
2		simp3	$⊢ (A \subseteq ℝ \land A \in Fin \land A \neq \emptyset) \to A \neq \emptyset$
3		fiminre2	$⊢ (A \subseteq ℝ \land A \in Fin) \to \exists x \in ℝ \forall y \in A x \leq y$
4	3	3adant3	$⊢ (A \subseteq ℝ \land A \in Fin \land A \neq \emptyset) \to \exists x \in ℝ \forall y \in A x \leq y$
5		infxrre	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to inf (A ℝ^{*} <) = inf (A ℝ <)$
6	1 2 4 5	syl3anc	$⊢ (A \subseteq ℝ \land A \in Fin \land A \neq \emptyset) \to inf (A ℝ^{*} <) = inf (A ℝ <)$

Metamath Proof Explorer