Metamath Proof Explorer


Theorem indf1ofs

Description: The bijection between finite subsets and the indicator functions with finite support. (Contributed by Thierry Arnoux, 22-Aug-2017)

Ref Expression
Assertion indf1ofs OV𝟙OFin:𝒫OFin1-1 ontof01O|f-11Fin

Proof

Step Hyp Ref Expression
1 indf1o OV𝟙O:𝒫O1-1 onto01O
2 f1of1 𝟙O:𝒫O1-1 onto01O𝟙O:𝒫O1-101O
3 1 2 syl OV𝟙O:𝒫O1-101O
4 inss1 𝒫OFin𝒫O
5 f1ores 𝟙O:𝒫O1-101O𝒫OFin𝒫O𝟙O𝒫OFin:𝒫OFin1-1 onto𝟙O𝒫OFin
6 3 4 5 sylancl OV𝟙O𝒫OFin:𝒫OFin1-1 onto𝟙O𝒫OFin
7 resres 𝟙O𝒫OFin=𝟙O𝒫OFin
8 f1ofn 𝟙O:𝒫O1-1 onto01O𝟙OFn𝒫O
9 fnresdm 𝟙OFn𝒫O𝟙O𝒫O=𝟙O
10 1 8 9 3syl OV𝟙O𝒫O=𝟙O
11 10 reseq1d OV𝟙O𝒫OFin=𝟙OFin
12 7 11 eqtr3id OV𝟙O𝒫OFin=𝟙OFin
13 eqidd OV𝒫OFin=𝒫OFin
14 simpll OVa𝒫OFin𝟙Oa=gOV
15 simpr OVa𝒫OFina𝒫OFin
16 4 15 sselid OVa𝒫OFina𝒫O
17 16 elpwid OVa𝒫OFinaO
18 indf OVaO𝟙Oa:O01
19 17 18 syldan OVa𝒫OFin𝟙Oa:O01
20 19 adantr OVa𝒫OFin𝟙Oa=g𝟙Oa:O01
21 simpr OVa𝒫OFin𝟙Oa=g𝟙Oa=g
22 21 feq1d OVa𝒫OFin𝟙Oa=g𝟙Oa:O01g:O01
23 20 22 mpbid OVa𝒫OFin𝟙Oa=gg:O01
24 prex 01V
25 elmapg 01VOVg01Og:O01
26 24 25 mpan OVg01Og:O01
27 26 biimpar OVg:O01g01O
28 14 23 27 syl2anc OVa𝒫OFin𝟙Oa=gg01O
29 21 cnveqd OVa𝒫OFin𝟙Oa=g𝟙Oa-1=g-1
30 29 imaeq1d OVa𝒫OFin𝟙Oa=g𝟙Oa-11=g-11
31 indpi1 OVaO𝟙Oa-11=a
32 17 31 syldan OVa𝒫OFin𝟙Oa-11=a
33 inss2 𝒫OFinFin
34 33 15 sselid OVa𝒫OFinaFin
35 32 34 eqeltrd OVa𝒫OFin𝟙Oa-11Fin
36 35 adantr OVa𝒫OFin𝟙Oa=g𝟙Oa-11Fin
37 30 36 eqeltrrd OVa𝒫OFin𝟙Oa=gg-11Fin
38 28 37 jca OVa𝒫OFin𝟙Oa=gg01Og-11Fin
39 38 rexlimdva2 OVa𝒫OFin𝟙Oa=gg01Og-11Fin
40 cnvimass g-11domg
41 26 biimpa OVg01Og:O01
42 41 fdmd OVg01Odomg=O
43 42 adantrr OVg01Og-11Findomg=O
44 40 43 sseqtrid OVg01Og-11Fing-11O
45 simprr OVg01Og-11Fing-11Fin
46 elfpw g-11𝒫OFing-11Og-11Fin
47 44 45 46 sylanbrc OVg01Og-11Fing-11𝒫OFin
48 indpreima OVg:O01g=𝟙Og-11
49 48 eqcomd OVg:O01𝟙Og-11=g
50 41 49 syldan OVg01O𝟙Og-11=g
51 50 adantrr OVg01Og-11Fin𝟙Og-11=g
52 fveqeq2 a=g-11𝟙Oa=g𝟙Og-11=g
53 52 rspcev g-11𝒫OFin𝟙Og-11=ga𝒫OFin𝟙Oa=g
54 47 51 53 syl2anc OVg01Og-11Fina𝒫OFin𝟙Oa=g
55 54 ex OVg01Og-11Fina𝒫OFin𝟙Oa=g
56 39 55 impbid OVa𝒫OFin𝟙Oa=gg01Og-11Fin
57 1 8 syl OV𝟙OFn𝒫O
58 fvelimab 𝟙OFn𝒫O𝒫OFin𝒫Og𝟙O𝒫OFina𝒫OFin𝟙Oa=g
59 57 4 58 sylancl OVg𝟙O𝒫OFina𝒫OFin𝟙Oa=g
60 cnveq f=gf-1=g-1
61 60 imaeq1d f=gf-11=g-11
62 61 eleq1d f=gf-11Fing-11Fin
63 62 elrab gf01O|f-11Fing01Og-11Fin
64 63 a1i OVgf01O|f-11Fing01Og-11Fin
65 56 59 64 3bitr4d OVg𝟙O𝒫OFingf01O|f-11Fin
66 65 eqrdv OV𝟙O𝒫OFin=f01O|f-11Fin
67 12 13 66 f1oeq123d OV𝟙O𝒫OFin:𝒫OFin1-1 onto𝟙O𝒫OFin𝟙OFin:𝒫OFin1-1 ontof01O|f-11Fin
68 6 67 mpbid OV𝟙OFin:𝒫OFin1-1 ontof01O|f-11Fin