Metamath Proof Explorer

Theorem rnmptbd2lem

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

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

Proof

Step Hyp Ref Expression
1 rnmptbd2lem.x 
 |-  F/ x ph
2 rnmptbd2lem.b 
 |-  ( ( ph /\ x e. A ) -> B e. V )
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 nfra1 
 |-  F/ x A. x e. A y <_ B
7 nfv 
 |-  F/ x y <_ z
8 rspa 
 |-  ( ( A. x e. A y <_ B /\ x e. A ) -> y <_ B )
9 simpl 
 |-  ( ( y <_ B /\ z = B ) -> y <_ B )
10 id 
 |-  ( z = B -> z = B )
11 10 eqcomd 
 |-  ( z = B -> B = z )
12 11 adantl 
 |-  ( ( y <_ B /\ z = B ) -> B = z )
13 9 12 breqtrd 
 |-  ( ( y <_ B /\ z = B ) -> y <_ z )
14 13 ex 
 |-  ( y <_ B -> ( z = B -> y <_ z ) )
15 8 14 syl 
 |-  ( ( A. x e. A y <_ B /\ x e. A ) -> ( z = B -> y <_ z ) )
16 15 ex 
 |-  ( A. x e. A y <_ B -> ( x e. A -> ( z = B -> y <_ z ) ) )
17 6 7 16 rexlimd 
 |-  ( A. x e. A y <_ B -> ( E. x e. A z = B -> y <_ z ) )
18 17 imp 
 |-  ( ( A. x e. A y <_ B /\ E. x e. A z = B ) -> y <_ z )
19 18 adantll 
 |-  ( ( ( ph /\ A. x e. A y <_ B ) /\ E. x e. A z = B ) -> y <_ z )
20 5 19 sylan2b 
 |-  ( ( ( ph /\ A. x e. A y <_ B ) /\ z e. ran ( x e. A |-> B ) ) -> y <_ z )
21 20 ralrimiva 
 |-  ( ( ph /\ A. x e. A y <_ B ) -> A. z e. ran ( x e. A |-> B ) y <_ z )
22 21 ex 
 |-  ( ph -> ( A. x e. A y <_ B -> A. z e. ran ( x e. A |-> B ) y <_ z ) )
23 22 reximdv 
 |-  ( ph -> ( E. y e. RR A. x e. A y <_ B -> E. y e. RR A. z e. ran ( x e. A |-> B ) y <_ z ) )
24 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
25 24 nfrn 
 |-  F/_ x ran ( x e. A |-> B )
26 25 7 nfralw 
 |-  F/ x A. z e. ran ( x e. A |-> B ) y <_ z
27 1 26 nfan 
 |-  F/ x ( ph /\ A. z e. ran ( x e. A |-> B ) y <_ z )
28 breq2 
 |-  ( z = B -> ( y <_ z <-> y <_ B ) )
29 simplr 
 |-  ( ( ( ph /\ A. z e. ran ( x e. A |-> B ) y <_ z ) /\ x e. A ) -> A. z e. ran ( x e. A |-> B ) y <_ z )
30 simpr 
 |-  ( ( ( ph /\ A. z e. ran ( x e. A |-> B ) y <_ z ) /\ x e. A ) -> x e. A )
31 2 adantlr 
 |-  ( ( ( ph /\ A. z e. ran ( x e. A |-> B ) y <_ z ) /\ x e. A ) -> B e. V )
32 3 30 31 elrnmpt1d 
 |-  ( ( ( ph /\ A. z e. ran ( x e. A |-> B ) y <_ z ) /\ x e. A ) -> B e. ran ( x e. A |-> B ) )
33 28 29 32 rspcdva 
 |-  ( ( ( ph /\ A. z e. ran ( x e. A |-> B ) y <_ z ) /\ x e. A ) -> y <_ B )
34 27 33 ralrimia 
 |-  ( ( ph /\ A. z e. ran ( x e. A |-> B ) y <_ z ) -> A. x e. A y <_ B )
35 34 ex 
 |-  ( ph -> ( A. z e. ran ( x e. A |-> B ) y <_ z -> A. x e. A y <_ B ) )
36 35 reximdv 
 |-  ( ph -> ( E. y e. RR A. z e. ran ( x e. A |-> B ) y <_ z -> E. y e. RR A. x e. A y <_ B ) )
37 23 36 impbid 
 |-  ( ph -> ( E. y e. RR A. x e. A y <_ B <-> E. y e. RR A. z e. ran ( x e. A |-> B ) y <_ z ) )