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

Metamath Proof Explorer

Theorem rnmptbddlem

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

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

Proof

Step Hyp Ref Expression
1 rnmptbddlem.x 
 |-  F/ x ph
2 rnmptbddlem.b 
 |-  ( ph -> E. y e. RR A. x e. A B <_ y )
3 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
4 3 elrnmpt 
 |-  ( z e. _V -> ( z e. ran ( x e. A |-> B ) <-> E. x e. A z = B ) )
5 4 elv 
 |-  ( z e. ran ( x e. A |-> B ) <-> E. x e. A z = B )
6 nfv 
 |-  F/ x y e. RR
7 1 6 nfan 
 |-  F/ x ( ph /\ y e. RR )
8 nfra1 
 |-  F/ x A. x e. A B <_ y
9 7 8 nfan 
 |-  F/ x ( ( ph /\ y e. RR ) /\ A. x e. A B <_ y )
10 nfv 
 |-  F/ x z <_ y
11 simp3 
 |-  ( ( A. x e. A B <_ y /\ x e. A /\ z = B ) -> z = B )
12 rspa 
 |-  ( ( A. x e. A B <_ y /\ x e. A ) -> B <_ y )
13 12 3adant3 
 |-  ( ( A. x e. A B <_ y /\ x e. A /\ z = B ) -> B <_ y )
14 11 13 eqbrtrd 
 |-  ( ( A. x e. A B <_ y /\ x e. A /\ z = B ) -> z <_ y )
15 14 3exp 
 |-  ( A. x e. A B <_ y -> ( x e. A -> ( z = B -> z <_ y ) ) )
16 15 adantl 
 |-  ( ( ( ph /\ y e. RR ) /\ A. x e. A B <_ y ) -> ( x e. A -> ( z = B -> z <_ y ) ) )
17 9 10 16 rexlimd 
 |-  ( ( ( ph /\ y e. RR ) /\ A. x e. A B <_ y ) -> ( E. x e. A z = B -> z <_ y ) )
18 17 imp 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. A B <_ y ) /\ E. x e. A z = B ) -> z <_ y )
19 5 18 sylan2b 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. A B <_ y ) /\ z e. ran ( x e. A |-> B ) ) -> z <_ y )
20 19 ralrimiva 
 |-  ( ( ( ph /\ y e. RR ) /\ A. x e. A B <_ y ) -> A. z e. ran ( x e. A |-> B ) z <_ y )
21 20 2 reximddv3 
 |-  ( ph -> E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y )