Theorem rnmptbdd

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

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

Proof

Step	Hyp	Ref	Expression
1		rnmptbdd.x	|- F/ x ph
2		rnmptbdd.b	|- ( ph -> E. y e. RR A. x e. A B <_ y )
3		breq2	|- ( y = v -> ( B <_ y <-> B <_ v ) )
4	3	ralbidv	|- ( y = v -> ( A. x e. A B <_ y <-> A. x e. A B <_ v ) )
5	4	cbvrexvw	|- ( E. y e. RR A. x e. A B <_ y <-> E. v e. RR A. x e. A B <_ v )
6	2 5	sylib	|- ( ph -> E. v e. RR A. x e. A B <_ v )
7	1 6	rnmptbddlem	|- ( ph -> E. v e. RR A. w e. ran ( x e. A |-> B ) w <_ v )
8		breq2	|- ( v = y -> ( w <_ v <-> w <_ y ) )
9	8	ralbidv	|- ( v = y -> ( A. w e. ran ( x e. A |-> B ) w <_ v <-> A. w e. ran ( x e. A |-> B ) w <_ y ) )
10		breq1	|- ( w = z -> ( w <_ y <-> z <_ y ) )
11	10	cbvralvw	|- ( A. w e. ran ( x e. A |-> B ) w <_ y <-> A. z e. ran ( x e. A |-> B ) z <_ y )
12	9 11	bitrdi	|- ( v = y -> ( A. w e. ran ( x e. A |-> B ) w <_ v <-> A. z e. ran ( x e. A |-> B ) z <_ y ) )
13	12	cbvrexvw	|- ( E. v e. RR A. w e. ran ( x e. A |-> B ) w <_ v <-> E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y )
14	7 13	sylib	|- ( ph -> E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y )