Theorem rnmptbd

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

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