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	|- F/ x ph
	fimaxre4.2	|- ( ph -> A e. Fin )
	fimaxre4.3	|- ( ( ph /\ x e. A ) -> B e. RR )
Assertion	fimaxre4	|- ( ph -> E. y e. RR A. x e. A B <_ y )

Proof

Step	Hyp	Ref	Expression
1		fimaxre4.1	|- F/ x ph
2		fimaxre4.2	|- ( ph -> A e. Fin )
3		fimaxre4.3	|- ( ( ph /\ x e. A ) -> B e. RR )
4	3	ex	|- ( ph -> ( x e. A -> B e. RR ) )
5	1 4	ralrimi	|- ( ph -> A. x e. A B e. RR )
6		fimaxre3	|- ( ( A e. Fin /\ A. x e. A B e. RR ) -> E. y e. RR A. x e. A B <_ y )
7	2 5 6	syl2anc	|- ( ph -> E. y e. RR A. x e. A B <_ y )