Theorem fimaxre4

Description: A nonempty finite set of real numbers is bounded (image set version). (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	fimaxre4.1	$$⊢Ⅎx\phi$$
	fimaxre4.2	$$⊢\phi \to A\in \mathrm{Fin}$$
	fimaxre4.3	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
Assertion	fimaxre4	$$⊢\phi \to \exists y\in ℝ\forall x\in AB\le y$$

Proof

Step	Hyp	Ref	Expression
1		fimaxre4.1	$$⊢Ⅎx\phi$$
2		fimaxre4.2	$$⊢\phi \to A\in \mathrm{Fin}$$
3		fimaxre4.3	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
4	3	ex	$$⊢\phi \to \left(x\in A\to B\in ℝ\right)$$
5	1 4	ralrimi	$$⊢\phi \to \forall x\in AB\in ℝ$$
6		fimaxre3	$$⊢\left(A\in \mathrm{Fin}\wedge \forall x\in AB\in ℝ\right)\to \exists y\in ℝ\forall x\in AB\le y$$
7	2 5 6	syl2anc	$$⊢\phi \to \exists y\in ℝ\forall x\in AB\le y$$