Description: A mapping being a finitely supported function in the family S . (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 11-Jul-2019) (Proof shortened by OpenAI, 30-Mar-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dprdff.w | |
|
dprdff.1 | |
||
dprdff.2 | |
||
dprdwd.3 | |
||
dprdwd.4 | |
||
Assertion | dprdwd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dprdff.w | |
|
2 | dprdff.1 | |
|
3 | dprdff.2 | |
|
4 | dprdwd.3 | |
|
5 | dprdwd.4 | |
|
6 | breq1 | |
|
7 | 4 | ralrimiva | |
8 | 2 3 | dprddomcld | |
9 | mptelixpg | |
|
10 | 8 9 | syl | |
11 | 7 10 | mpbird | |
12 | fveq2 | |
|
13 | 12 | cbvixpv | |
14 | 11 13 | eleqtrdi | |
15 | 6 14 5 | elrabd | |
16 | 15 1 | eleqtrrdi | |