Theorem rnmptbddlem

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

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

Proof

Step	Hyp	Ref	Expression
1		rnmptbddlem.x	|- F/ x ph
2		rnmptbddlem.b	|- ( ph -> E. y e. RR A. x e. A B <_ y )
3		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
4	3	elrnmpt	|- ( z e. _V -> ( z e. ran ( x e. A |-> B ) <-> E. x e. A z = B ) )
5	4	elv	|- ( z e. ran ( x e. A |-> B ) <-> E. x e. A z = B )
6		nfv	|- F/ x y e. RR
7	1 6	nfan	|- F/ x ( ph /\ y e. RR )
8		nfra1	|- F/ x A. x e. A B <_ y
9	7 8	nfan	|- F/ x ( ( ph /\ y e. RR ) /\ A. x e. A B <_ y )
10		nfv	|- F/ x z <_ y
11		simp3	|- ( ( A. x e. A B <_ y /\ x e. A /\ z = B ) -> z = B )
12		rspa	|- ( ( A. x e. A B <_ y /\ x e. A ) -> B <_ y )
13	12	3adant3	|- ( ( A. x e. A B <_ y /\ x e. A /\ z = B ) -> B <_ y )
14	11 13	eqbrtrd	|- ( ( A. x e. A B <_ y /\ x e. A /\ z = B ) -> z <_ y )
15	14	3exp	|- ( A. x e. A B <_ y -> ( x e. A -> ( z = B -> z <_ y ) ) )
16	15	adantl	|- ( ( ( ph /\ y e. RR ) /\ A. x e. A B <_ y ) -> ( x e. A -> ( z = B -> z <_ y ) ) )
17	9 10 16	rexlimd	|- ( ( ( ph /\ y e. RR ) /\ A. x e. A B <_ y ) -> ( E. x e. A z = B -> z <_ y ) )
18	17	imp	|- ( ( ( ( ph /\ y e. RR ) /\ A. x e. A B <_ y ) /\ E. x e. A z = B ) -> z <_ y )
19	5 18	sylan2b	|- ( ( ( ( ph /\ y e. RR ) /\ A. x e. A B <_ y ) /\ z e. ran ( x e. A |-> B ) ) -> z <_ y )
20	19	ralrimiva	|- ( ( ( ph /\ y e. RR ) /\ A. x e. A B <_ y ) -> A. z e. ran ( x e. A |-> B ) z <_ y )
21	20 2	reximddv3	|- ( ph -> E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y )