Metamath Proof Explorer


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 x φ
rnmptbd.b φ x A B V
Assertion rnmptbd φ y x A B y y z ran x A B z y

Proof

Step Hyp Ref Expression
1 rnmptbd.x x φ
2 rnmptbd.b φ x A B V
3 breq2 y = w B y B w
4 3 ralbidv y = w x A B y x A B w
5 4 cbvrexvw y x A B y w x A B w
6 5 a1i φ y x A B y w x A B w
7 nfv w φ
8 1 7 2 rnmptbdlem φ w x A B w w u ran x A B u w
9 breq2 w = y u w u y
10 9 ralbidv w = y u ran x A B u w u ran x A B u y
11 breq1 u = z u y z y
12 11 cbvralvw u ran x A B u y z ran x A B z y
13 10 12 bitrdi w = y u ran x A B u w z ran x A B z y
14 13 cbvrexvw w u ran x A B u w y z ran x A B z y
15 14 a1i φ w u ran x A B u w y z ran x A B z y
16 6 8 15 3bitrd φ y x A B y y z ran x A B z y