This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )