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

Metamath Proof Explorer

Theorem rnmptbd2

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

Ref Expression
Hypotheses rnmptbd2.x 
|- F/ x ph
rnmptbd2.b 
|- ( ( ph /\ x e. A ) -> B e. V )
Assertion rnmptbd2 
|- ( 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 rnmptbd2.x 
 |-  F/ x ph
2 rnmptbd2.b 
 |-  ( ( ph /\ x e. A ) -> B e. V )
3 breq1 
 |-  ( y = w -> ( y <_ B <-> w <_ B ) )
4 3 ralbidv 
 |-  ( y = w -> ( A. x e. A y <_ B <-> A. x e. A w <_ B ) )
5 4 cbvrexvw 
 |-  ( E. y e. RR A. x e. A y <_ B <-> E. w e. RR A. x e. A w <_ B )
6 5 a1i 
 |-  ( ph -> ( E. y e. RR A. x e. A y <_ B <-> E. w e. RR A. x e. A w <_ B ) )
7 1 2 rnmptbd2lem 
 |-  ( ph -> ( E. w e. RR A. x e. A w <_ B <-> E. w e. RR A. u e. ran ( x e. A |-> B ) w <_ u ) )
8 breq1 
 |-  ( w = y -> ( w <_ u <-> y <_ u ) )
9 8 ralbidv 
 |-  ( w = y -> ( A. u e. ran ( x e. A |-> B ) w <_ u <-> A. u e. ran ( x e. A |-> B ) y <_ u ) )
10 breq2 
 |-  ( u = z -> ( y <_ u <-> y <_ z ) )
11 10 cbvralvw 
 |-  ( A. u e. ran ( x e. A |-> B ) y <_ u <-> A. z e. ran ( x e. A |-> B ) y <_ z )
12 9 11 bitrdi 
 |-  ( w = y -> ( A. u e. ran ( x e. A |-> B ) w <_ u <-> A. z e. ran ( x e. A |-> B ) y <_ z ) )
13 12 cbvrexvw 
 |-  ( E. w e. RR A. u e. ran ( x e. A |-> B ) w <_ u <-> E. y e. RR A. z e. ran ( x e. A |-> B ) y <_ z )
14 13 a1i 
 |-  ( ph -> ( E. w e. RR A. u e. ran ( x e. A |-> B ) w <_ u <-> E. y e. RR A. z e. ran ( x e. A |-> B ) y <_ z ) )
15 6 7 14 3bitrd 
 |-  ( 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 ) )