Metamath Proof Explorer

Theorem rnmptbdlem

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

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

Proof

Step Hyp Ref Expression
1 rnmptbdlem.x 
 |-  F/ x ph
2 rnmptbdlem.y 
 |-  F/ y ph
3 rnmptbdlem.b 
 |-  ( ( ph /\ x e. A ) -> B e. V )
4 nfcv 
 |-  F/_ x RR
5 nfra1 
 |-  F/ x A. x e. A B <_ y
6 4 5 nfrex 
 |-  F/ x E. y e. RR A. x e. A B <_ y
7 1 6 nfan 
 |-  F/ x ( ph /\ E. y e. RR A. x e. A B <_ y )
8 simpr 
 |-  ( ( ph /\ E. y e. RR A. x e. A B <_ y ) -> E. y e. RR A. x e. A B <_ y )
9 7 8 rnmptbdd 
 |-  ( ( ph /\ E. y e. RR A. x e. A B <_ y ) -> E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y )
10 9 ex 
 |-  ( ph -> ( E. y e. RR A. x e. A B <_ y -> E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y ) )
11 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
12 11 nfrn 
 |-  F/_ x ran ( x e. A |-> B )
13 nfv 
 |-  F/ x z <_ y
14 12 13 nfralw 
 |-  F/ x A. z e. ran ( x e. A |-> B ) z <_ y
15 1 14 nfan 
 |-  F/ x ( ph /\ A. z e. ran ( x e. A |-> B ) z <_ y )
16 breq1 
 |-  ( z = B -> ( z <_ y <-> B <_ y ) )
17 simplr 
 |-  ( ( ( ph /\ A. z e. ran ( x e. A |-> B ) z <_ y ) /\ x e. A ) -> A. z e. ran ( x e. A |-> B ) z <_ y )
18 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
19 simpr 
 |-  ( ( ( ph /\ A. z e. ran ( x e. A |-> B ) z <_ y ) /\ x e. A ) -> x e. A )
20 3 adantlr 
 |-  ( ( ( ph /\ A. z e. ran ( x e. A |-> B ) z <_ y ) /\ x e. A ) -> B e. V )
21 18 19 20 elrnmpt1d 
 |-  ( ( ( ph /\ A. z e. ran ( x e. A |-> B ) z <_ y ) /\ x e. A ) -> B e. ran ( x e. A |-> B ) )
22 16 17 21 rspcdva 
 |-  ( ( ( ph /\ A. z e. ran ( x e. A |-> B ) z <_ y ) /\ x e. A ) -> B <_ y )
23 15 22 ralrimia 
 |-  ( ( ph /\ A. z e. ran ( x e. A |-> B ) z <_ y ) -> A. x e. A B <_ y )
24 23 ex 
 |-  ( ph -> ( A. z e. ran ( x e. A |-> B ) z <_ y -> A. x e. A B <_ y ) )
25 24 a1d 
 |-  ( ph -> ( y e. RR -> ( A. z e. ran ( x e. A |-> B ) z <_ y -> A. x e. A B <_ y ) ) )
26 2 25 reximdai 
 |-  ( ph -> ( E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y -> E. y e. RR A. x e. A B <_ y ) )
27 10 26 impbid 
 |-  ( ph -> ( E. y e. RR A. x e. A B <_ y <-> E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y ) )