Metamath Proof Explorer


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 )