Metamath Proof Explorer


Theorem rnmptbdd

Description: Boundness of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses rnmptbdd.x
|- F/ x ph
rnmptbdd.b
|- ( ph -> E. y e. RR A. x e. A B <_ y )
Assertion rnmptbdd
|- ( ph -> E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y )

Proof

Step Hyp Ref Expression
1 rnmptbdd.x
 |-  F/ x ph
2 rnmptbdd.b
 |-  ( ph -> E. y e. RR A. x e. A B <_ y )
3 breq2
 |-  ( y = v -> ( B <_ y <-> B <_ v ) )
4 3 ralbidv
 |-  ( y = v -> ( A. x e. A B <_ y <-> A. x e. A B <_ v ) )
5 4 cbvrexvw
 |-  ( E. y e. RR A. x e. A B <_ y <-> E. v e. RR A. x e. A B <_ v )
6 2 5 sylib
 |-  ( ph -> E. v e. RR A. x e. A B <_ v )
7 1 6 rnmptbddlem
 |-  ( ph -> E. v e. RR A. w e. ran ( x e. A |-> B ) w <_ v )
8 breq2
 |-  ( v = y -> ( w <_ v <-> w <_ y ) )
9 8 ralbidv
 |-  ( v = y -> ( A. w e. ran ( x e. A |-> B ) w <_ v <-> A. w e. ran ( x e. A |-> B ) w <_ y ) )
10 breq1
 |-  ( w = z -> ( w <_ y <-> z <_ y ) )
11 10 cbvralvw
 |-  ( A. w e. ran ( x e. A |-> B ) w <_ y <-> A. z e. ran ( x e. A |-> B ) z <_ y )
12 9 11 bitrdi
 |-  ( v = y -> ( A. w e. ran ( x e. A |-> B ) w <_ v <-> A. z e. ran ( x e. A |-> B ) z <_ y ) )
13 12 cbvrexvw
 |-  ( E. v e. RR A. w e. ran ( x e. A |-> B ) w <_ v <-> E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y )
14 7 13 sylib
 |-  ( ph -> E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y )