Metamath Proof Explorer


Theorem rnmptbd2lem

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

Ref Expression
Hypotheses rnmptbd2lem.x xφ
rnmptbd2lem.b φxABV
Assertion rnmptbd2lem φyxAyByzranxAByz

Proof

Step Hyp Ref Expression
1 rnmptbd2lem.x xφ
2 rnmptbd2lem.b φxABV
3 eqid xAB=xAB
4 3 elrnmpt zVzranxABxAz=B
5 4 elv zranxABxAz=B
6 nfra1 xxAyB
7 nfv xyz
8 rspa xAyBxAyB
9 simpl yBz=ByB
10 id z=Bz=B
11 10 eqcomd z=BB=z
12 11 adantl yBz=BB=z
13 9 12 breqtrd yBz=Byz
14 13 ex yBz=Byz
15 8 14 syl xAyBxAz=Byz
16 15 ex xAyBxAz=Byz
17 6 7 16 rexlimd xAyBxAz=Byz
18 17 imp xAyBxAz=Byz
19 18 adantll φxAyBxAz=Byz
20 5 19 sylan2b φxAyBzranxAByz
21 20 ralrimiva φxAyBzranxAByz
22 21 ex φxAyBzranxAByz
23 22 reximdv φyxAyByzranxAByz
24 nfmpt1 _xxAB
25 24 nfrn _xranxAB
26 25 7 nfralw xzranxAByz
27 1 26 nfan xφzranxAByz
28 breq2 z=ByzyB
29 simplr φzranxAByzxAzranxAByz
30 simpr φzranxAByzxAxA
31 2 adantlr φzranxAByzxABV
32 3 30 31 elrnmpt1d φzranxAByzxABranxAB
33 28 29 32 rspcdva φzranxAByzxAyB
34 27 33 ralrimia φzranxAByzxAyB
35 34 ex φzranxAByzxAyB
36 35 reximdv φyzranxAByzyxAyB
37 23 36 impbid φyxAyByzranxAByz