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

Metamath Proof Explorer

Theorem rnmptlb

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

Ref Expression
Hypothesis rnmptlb.1 
|- ( ph -> E. y e. RR A. x e. A y <_ B )
Assertion rnmptlb 
|- ( ph -> E. y e. RR A. z e. ran ( x e. A |-> B ) y <_ z )

Proof

Step Hyp Ref Expression
1 rnmptlb.1 
 |-  ( ph -> E. y e. RR A. x e. A y <_ B )
2 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
3 2 elrnmpt 
 |-  ( z e. _V -> ( z e. ran ( x e. A |-> B ) <-> E. x e. A z = B ) )
4 3 elv 
 |-  ( z e. ran ( x e. A |-> B ) <-> E. x e. A z = B )
5 nfra1 
 |-  F/ x A. x e. A w <_ B
6 nfv 
 |-  F/ x w <_ z
7 rspa 
 |-  ( ( A. x e. A w <_ B /\ x e. A ) -> w <_ B )
8 7 3adant3 
 |-  ( ( A. x e. A w <_ B /\ x e. A /\ z = B ) -> w <_ B )
9 simp3 
 |-  ( ( A. x e. A w <_ B /\ x e. A /\ z = B ) -> z = B )
10 8 9 breqtrrd 
 |-  ( ( A. x e. A w <_ B /\ x e. A /\ z = B ) -> w <_ z )
11 10 3exp 
 |-  ( A. x e. A w <_ B -> ( x e. A -> ( z = B -> w <_ z ) ) )
12 5 6 11 rexlimd 
 |-  ( A. x e. A w <_ B -> ( E. x e. A z = B -> w <_ z ) )
13 12 imp 
 |-  ( ( A. x e. A w <_ B /\ E. x e. A z = B ) -> w <_ z )
14 13 adantll 
 |-  ( ( ( ( ph /\ w e. RR ) /\ A. x e. A w <_ B ) /\ E. x e. A z = B ) -> w <_ z )
15 4 14 sylan2b 
 |-  ( ( ( ( ph /\ w e. RR ) /\ A. x e. A w <_ B ) /\ z e. ran ( x e. A |-> B ) ) -> w <_ z )
16 15 ralrimiva 
 |-  ( ( ( ph /\ w e. RR ) /\ A. x e. A w <_ B ) -> A. z e. ran ( x e. A |-> B ) w <_ z )
17 breq1 
 |-  ( y = w -> ( y <_ B <-> w <_ B ) )
18 17 ralbidv 
 |-  ( y = w -> ( A. x e. A y <_ B <-> A. x e. A w <_ B ) )
19 18 cbvrexvw 
 |-  ( E. y e. RR A. x e. A y <_ B <-> E. w e. RR A. x e. A w <_ B )
20 1 19 sylib 
 |-  ( ph -> E. w e. RR A. x e. A w <_ B )
21 16 20 reximddv3 
 |-  ( ph -> E. w e. RR A. z e. ran ( x e. A |-> B ) w <_ z )
22 breq1 
 |-  ( w = y -> ( w <_ z <-> y <_ z ) )
23 22 ralbidv 
 |-  ( w = y -> ( A. z e. ran ( x e. A |-> B ) w <_ z <-> A. z e. ran ( x e. A |-> B ) y <_ z ) )
24 23 cbvrexvw 
 |-  ( E. w e. RR A. z e. ran ( x e. A |-> B ) w <_ z <-> E. y e. RR A. z e. ran ( x e. A |-> B ) y <_ z )
25 21 24 sylib 
 |-  ( ph -> E. y e. RR A. z e. ran ( x e. A |-> B ) y <_ z )