Metamath Proof Explorer


Theorem fpwrelmapffs

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 AV
fpwrelmap.2 BV
fpwrelmap.3 M=f𝒫BAxy|xAyfx
fpwrelmapffs.1 S=f𝒫BFinA|fsuppFin
Assertion fpwrelmapffs MS:S1-1 onto𝒫A×BFin

Proof

Step Hyp Ref Expression
1 fpwrelmap.1 AV
2 fpwrelmap.2 BV
3 fpwrelmap.3 M=f𝒫BAxy|xAyfx
4 fpwrelmapffs.1 S=f𝒫BFinA|fsuppFin
5 1 2 3 fpwrelmap M:𝒫BA1-1 onto𝒫A×B
6 5 a1i M:𝒫BA1-1 onto𝒫A×B
7 simpl f𝒫BAr=xy|xAyfxf𝒫BA
8 2 pwex 𝒫BV
9 8 1 elmap f𝒫BAf:A𝒫B
10 7 9 sylib f𝒫BAr=xy|xAyfxf:A𝒫B
11 simpr f𝒫BAr=xy|xAyfxr=xy|xAyfx
12 1 2 10 11 fpwrelmapffslem f𝒫BAr=xy|xAyfxrFinranfFinfsuppFin
13 12 3adant1 f𝒫BAr=xy|xAyfxrFinranfFinfsuppFin
14 3 6 13 f1oresrab Mf𝒫BA|ranfFinfsuppFin:f𝒫BA|ranfFinfsuppFin1-1 ontor𝒫A×B|rFin
15 14 mptru Mf𝒫BA|ranfFinfsuppFin:f𝒫BA|ranfFinfsuppFin1-1 ontor𝒫A×B|rFin
16 1 8 maprnin 𝒫BFinA=f𝒫BA|ranfFin
17 nfcv _f𝒫BFinA
18 nfrab1 _ff𝒫BA|ranfFin
19 17 18 rabeqf 𝒫BFinA=f𝒫BA|ranfFinf𝒫BFinA|fsuppFin=ff𝒫BA|ranfFin|fsuppFin
20 16 19 ax-mp f𝒫BFinA|fsuppFin=ff𝒫BA|ranfFin|fsuppFin
21 rabrab ff𝒫BA|ranfFin|fsuppFin=f𝒫BA|ranfFinfsuppFin
22 4 20 21 3eqtri S=f𝒫BA|ranfFinfsuppFin
23 dfin5 𝒫A×BFin=r𝒫A×B|rFin
24 f1oeq23 S=f𝒫BA|ranfFinfsuppFin𝒫A×BFin=r𝒫A×B|rFinMS:S1-1 onto𝒫A×BFinMS:f𝒫BA|ranfFinfsuppFin1-1 ontor𝒫A×B|rFin
25 22 23 24 mp2an MS:S1-1 onto𝒫A×BFinMS:f𝒫BA|ranfFinfsuppFin1-1 ontor𝒫A×B|rFin
26 22 reseq2i MS=Mf𝒫BA|ranfFinfsuppFin
27 f1oeq1 MS=Mf𝒫BA|ranfFinfsuppFinMS:f𝒫BA|ranfFinfsuppFin1-1 ontor𝒫A×B|rFinMf𝒫BA|ranfFinfsuppFin:f𝒫BA|ranfFinfsuppFin1-1 ontor𝒫A×B|rFin
28 26 27 ax-mp MS:f𝒫BA|ranfFinfsuppFin1-1 ontor𝒫A×B|rFinMf𝒫BA|ranfFinfsuppFin:f𝒫BA|ranfFinfsuppFin1-1 ontor𝒫A×B|rFin
29 25 28 bitr2i Mf𝒫BA|ranfFinfsuppFin:f𝒫BA|ranfFinfsuppFin1-1 ontor𝒫A×B|rFinMS:S1-1 onto𝒫A×BFin
30 15 29 mpbi MS:S1-1 onto𝒫A×BFin