Description: Define a canonical mapping between finite relations (finite subsets of a cartesian product) and functions with finite support into finite subsets. (Contributed by Thierry Arnoux, 28-Aug-2017) (Revised by Thierry Arnoux, 1-Sep-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fpwrelmap.1 | |
|
fpwrelmap.2 | |
||
fpwrelmap.3 | |
||
fpwrelmapffs.1 | |
||
Assertion | fpwrelmapffs | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fpwrelmap.1 | |
|
2 | fpwrelmap.2 | |
|
3 | fpwrelmap.3 | |
|
4 | fpwrelmapffs.1 | |
|
5 | 1 2 3 | fpwrelmap | |
6 | 5 | a1i | |
7 | simpl | |
|
8 | 2 | pwex | |
9 | 8 1 | elmap | |
10 | 7 9 | sylib | |
11 | simpr | |
|
12 | 1 2 10 11 | fpwrelmapffslem | |
13 | 12 | 3adant1 | |
14 | 3 6 13 | f1oresrab | |
15 | 14 | mptru | |
16 | 1 8 | maprnin | |
17 | nfcv | |
|
18 | nfrab1 | |
|
19 | 17 18 | rabeqf | |
20 | 16 19 | ax-mp | |
21 | rabrab | |
|
22 | 4 20 21 | 3eqtri | |
23 | dfin5 | |
|
24 | f1oeq23 | |
|
25 | 22 23 24 | mp2an | |
26 | 22 | reseq2i | |
27 | f1oeq1 | |
|
28 | 26 27 | ax-mp | |
29 | 25 28 | bitr2i | |
30 | 15 29 | mpbi | |