Metamath Proof Explorer


Theorem rnmptbdlem

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

Ref Expression
Hypotheses rnmptbdlem.x x φ
rnmptbdlem.y y φ
rnmptbdlem.b φ x A B V
Assertion rnmptbdlem φ y x A B y y z ran x A B z y

Proof

Step Hyp Ref Expression
1 rnmptbdlem.x x φ
2 rnmptbdlem.y y φ
3 rnmptbdlem.b φ x A B V
4 nfcv _ x
5 nfra1 x x A B y
6 4 5 nfrex x y x A B y
7 1 6 nfan x φ y x A B y
8 simpr φ y x A B y y x A B y
9 7 8 rnmptbdd φ y x A B y y z ran x A B z y
10 9 ex φ y x A B y y z ran x A B z y
11 nfmpt1 _ x x A B
12 11 nfrn _ x ran x A B
13 nfv x z y
14 12 13 nfralw x z ran x A B z y
15 1 14 nfan x φ z ran x A B z y
16 breq1 z = B z y B y
17 simplr φ z ran x A B z y x A z ran x A B z y
18 eqid x A B = x A B
19 simpr φ z ran x A B z y x A x A
20 3 adantlr φ z ran x A B z y x A B V
21 18 19 20 elrnmpt1d φ z ran x A B z y x A B ran x A B
22 16 17 21 rspcdva φ z ran x A B z y x A B y
23 15 22 ralrimia φ z ran x A B z y x A B y
24 23 ex φ z ran x A B z y x A B y
25 24 a1d φ y z ran x A B z y x A B y
26 2 25 reximdai φ y z ran x A B z y y x A B y
27 10 26 impbid φ y x A B y y z ran x A B z y