Description: The bijection between finite subsets and the indicator functions with finite support. (Contributed by Thierry Arnoux, 22-Aug-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | indf1ofs | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | indf1o | |
|
2 | f1of1 | |
|
3 | 1 2 | syl | |
4 | inss1 | |
|
5 | f1ores | |
|
6 | 3 4 5 | sylancl | |
7 | resres | |
|
8 | f1ofn | |
|
9 | fnresdm | |
|
10 | 1 8 9 | 3syl | |
11 | 10 | reseq1d | |
12 | 7 11 | eqtr3id | |
13 | eqidd | |
|
14 | simpll | |
|
15 | simpr | |
|
16 | 4 15 | sselid | |
17 | 16 | elpwid | |
18 | indf | |
|
19 | 17 18 | syldan | |
20 | 19 | adantr | |
21 | simpr | |
|
22 | 21 | feq1d | |
23 | 20 22 | mpbid | |
24 | prex | |
|
25 | elmapg | |
|
26 | 24 25 | mpan | |
27 | 26 | biimpar | |
28 | 14 23 27 | syl2anc | |
29 | 21 | cnveqd | |
30 | 29 | imaeq1d | |
31 | indpi1 | |
|
32 | 17 31 | syldan | |
33 | inss2 | |
|
34 | 33 15 | sselid | |
35 | 32 34 | eqeltrd | |
36 | 35 | adantr | |
37 | 30 36 | eqeltrrd | |
38 | 28 37 | jca | |
39 | 38 | rexlimdva2 | |
40 | cnvimass | |
|
41 | 26 | biimpa | |
42 | 41 | fdmd | |
43 | 42 | adantrr | |
44 | 40 43 | sseqtrid | |
45 | simprr | |
|
46 | elfpw | |
|
47 | 44 45 46 | sylanbrc | |
48 | indpreima | |
|
49 | 48 | eqcomd | |
50 | 41 49 | syldan | |
51 | 50 | adantrr | |
52 | fveqeq2 | |
|
53 | 52 | rspcev | |
54 | 47 51 53 | syl2anc | |
55 | 54 | ex | |
56 | 39 55 | impbid | |
57 | 1 8 | syl | |
58 | fvelimab | |
|
59 | 57 4 58 | sylancl | |
60 | cnveq | |
|
61 | 60 | imaeq1d | |
62 | 61 | eleq1d | |
63 | 62 | elrab | |
64 | 63 | a1i | |
65 | 56 59 64 | 3bitr4d | |
66 | 65 | eqrdv | |
67 | 12 13 66 | f1oeq123d | |
68 | 6 67 | mpbid | |