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 | |
|
rnmptbd2lem.b | |
||
Assertion | rnmptbd2lem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rnmptbd2lem.x | |
|
2 | rnmptbd2lem.b | |
|
3 | eqid | |
|
4 | 3 | elrnmpt | |
5 | 4 | elv | |
6 | nfra1 | |
|
7 | nfv | |
|
8 | rspa | |
|
9 | simpl | |
|
10 | id | |
|
11 | 10 | eqcomd | |
12 | 11 | adantl | |
13 | 9 12 | breqtrd | |
14 | 13 | ex | |
15 | 8 14 | syl | |
16 | 15 | ex | |
17 | 6 7 16 | rexlimd | |
18 | 17 | imp | |
19 | 18 | adantll | |
20 | 5 19 | sylan2b | |
21 | 20 | ralrimiva | |
22 | 21 | ex | |
23 | 22 | reximdv | |
24 | nfmpt1 | |
|
25 | 24 | nfrn | |
26 | 25 7 | nfralw | |
27 | 1 26 | nfan | |
28 | breq2 | |
|
29 | simplr | |
|
30 | simpr | |
|
31 | 2 | adantlr | |
32 | 3 30 31 | elrnmpt1d | |
33 | 28 29 32 | rspcdva | |
34 | 27 33 | ralrimia | |
35 | 34 | ex | |
36 | 35 | reximdv | |
37 | 23 36 | impbid | |