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 ) )