Metamath Proof Explorer


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

Proof

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