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 
|- ( O e. V -> ( ( _Ind ` O ) |` Fin ) : ( ~P O i^i Fin ) -1-1-onto-> { f e. ( { 0 , 1 } ^m O ) | ( `' f " { 1 } ) e. Fin } )

Proof

Step Hyp Ref Expression
1 indf1o 
 |-  ( O e. V -> ( _Ind ` O ) : ~P O -1-1-onto-> ( { 0 , 1 } ^m O ) )
2 f1of1 
 |-  ( ( _Ind ` O ) : ~P O -1-1-onto-> ( { 0 , 1 } ^m O ) -> ( _Ind ` O ) : ~P O -1-1-> ( { 0 , 1 } ^m O ) )
3 1 2 syl 
 |-  ( O e. V -> ( _Ind ` O ) : ~P O -1-1-> ( { 0 , 1 } ^m O ) )
4 inss1 
 |-  ( ~P O i^i Fin ) C_ ~P O
5 f1ores 
 |-  ( ( ( _Ind ` O ) : ~P O -1-1-> ( { 0 , 1 } ^m O ) /\ ( ~P O i^i Fin ) C_ ~P O ) -> ( ( _Ind ` O ) |` ( ~P O i^i Fin ) ) : ( ~P O i^i Fin ) -1-1-onto-> ( ( _Ind ` O ) " ( ~P O i^i Fin ) ) )
6 3 4 5 sylancl 
 |-  ( O e. V -> ( ( _Ind ` O ) |` ( ~P O i^i Fin ) ) : ( ~P O i^i Fin ) -1-1-onto-> ( ( _Ind ` O ) " ( ~P O i^i Fin ) ) )
7 resres 
 |-  ( ( ( _Ind ` O ) |` ~P O ) |` Fin ) = ( ( _Ind ` O ) |` ( ~P O i^i Fin ) )
8 f1ofn 
 |-  ( ( _Ind ` O ) : ~P O -1-1-onto-> ( { 0 , 1 } ^m O ) -> ( _Ind ` O ) Fn ~P O )
9 fnresdm 
 |-  ( ( _Ind ` O ) Fn ~P O -> ( ( _Ind ` O ) |` ~P O ) = ( _Ind ` O ) )
10 1 8 9 3syl 
 |-  ( O e. V -> ( ( _Ind ` O ) |` ~P O ) = ( _Ind ` O ) )
11 10 reseq1d 
 |-  ( O e. V -> ( ( ( _Ind ` O ) |` ~P O ) |` Fin ) = ( ( _Ind ` O ) |` Fin ) )
12 7 11 eqtr3id 
 |-  ( O e. V -> ( ( _Ind ` O ) |` ( ~P O i^i Fin ) ) = ( ( _Ind ` O ) |` Fin ) )
13 eqidd 
 |-  ( O e. V -> ( ~P O i^i Fin ) = ( ~P O i^i Fin ) )
14 simpll 
 |-  ( ( ( O e. V /\ a e. ( ~P O i^i Fin ) ) /\ ( ( _Ind ` O ) ` a ) = g ) -> O e. V )
15 simpr 
 |-  ( ( O e. V /\ a e. ( ~P O i^i Fin ) ) -> a e. ( ~P O i^i Fin ) )
16 4 15 sselid 
 |-  ( ( O e. V /\ a e. ( ~P O i^i Fin ) ) -> a e. ~P O )
17 16 elpwid 
 |-  ( ( O e. V /\ a e. ( ~P O i^i Fin ) ) -> a C_ O )
18 indf 
 |-  ( ( O e. V /\ a C_ O ) -> ( ( _Ind ` O ) ` a ) : O --> { 0 , 1 } )
19 17 18 syldan 
 |-  ( ( O e. V /\ a e. ( ~P O i^i Fin ) ) -> ( ( _Ind ` O ) ` a ) : O --> { 0 , 1 } )
20 19 adantr 
 |-  ( ( ( O e. V /\ a e. ( ~P O i^i Fin ) ) /\ ( ( _Ind ` O ) ` a ) = g ) -> ( ( _Ind ` O ) ` a ) : O --> { 0 , 1 } )
21 simpr 
 |-  ( ( ( O e. V /\ a e. ( ~P O i^i Fin ) ) /\ ( ( _Ind ` O ) ` a ) = g ) -> ( ( _Ind ` O ) ` a ) = g )
22 21 feq1d 
 |-  ( ( ( O e. V /\ a e. ( ~P O i^i Fin ) ) /\ ( ( _Ind ` O ) ` a ) = g ) -> ( ( ( _Ind ` O ) ` a ) : O --> { 0 , 1 } <-> g : O --> { 0 , 1 } ) )
23 20 22 mpbid 
 |-  ( ( ( O e. V /\ a e. ( ~P O i^i Fin ) ) /\ ( ( _Ind ` O ) ` a ) = g ) -> g : O --> { 0 , 1 } )
24 prex 
 |-  { 0 , 1 } e. _V
25 elmapg 
 |-  ( ( { 0 , 1 } e. _V /\ O e. V ) -> ( g e. ( { 0 , 1 } ^m O ) <-> g : O --> { 0 , 1 } ) )
26 24 25 mpan 
 |-  ( O e. V -> ( g e. ( { 0 , 1 } ^m O ) <-> g : O --> { 0 , 1 } ) )
27 26 biimpar 
 |-  ( ( O e. V /\ g : O --> { 0 , 1 } ) -> g e. ( { 0 , 1 } ^m O ) )
28 14 23 27 syl2anc 
 |-  ( ( ( O e. V /\ a e. ( ~P O i^i Fin ) ) /\ ( ( _Ind ` O ) ` a ) = g ) -> g e. ( { 0 , 1 } ^m O ) )
29 21 cnveqd 
 |-  ( ( ( O e. V /\ a e. ( ~P O i^i Fin ) ) /\ ( ( _Ind ` O ) ` a ) = g ) -> `' ( ( _Ind ` O ) ` a ) = `' g )
30 29 imaeq1d 
 |-  ( ( ( O e. V /\ a e. ( ~P O i^i Fin ) ) /\ ( ( _Ind ` O ) ` a ) = g ) -> ( `' ( ( _Ind ` O ) ` a ) " { 1 } ) = ( `' g " { 1 } ) )
31 indpi1 
 |-  ( ( O e. V /\ a C_ O ) -> ( `' ( ( _Ind ` O ) ` a ) " { 1 } ) = a )
32 17 31 syldan 
 |-  ( ( O e. V /\ a e. ( ~P O i^i Fin ) ) -> ( `' ( ( _Ind ` O ) ` a ) " { 1 } ) = a )
33 inss2 
 |-  ( ~P O i^i Fin ) C_ Fin
34 33 15 sselid 
 |-  ( ( O e. V /\ a e. ( ~P O i^i Fin ) ) -> a e. Fin )
35 32 34 eqeltrd 
 |-  ( ( O e. V /\ a e. ( ~P O i^i Fin ) ) -> ( `' ( ( _Ind ` O ) ` a ) " { 1 } ) e. Fin )
36 35 adantr 
 |-  ( ( ( O e. V /\ a e. ( ~P O i^i Fin ) ) /\ ( ( _Ind ` O ) ` a ) = g ) -> ( `' ( ( _Ind ` O ) ` a ) " { 1 } ) e. Fin )
37 30 36 eqeltrrd 
 |-  ( ( ( O e. V /\ a e. ( ~P O i^i Fin ) ) /\ ( ( _Ind ` O ) ` a ) = g ) -> ( `' g " { 1 } ) e. Fin )
38 28 37 jca 
 |-  ( ( ( O e. V /\ a e. ( ~P O i^i Fin ) ) /\ ( ( _Ind ` O ) ` a ) = g ) -> ( g e. ( { 0 , 1 } ^m O ) /\ ( `' g " { 1 } ) e. Fin ) )
39 38 rexlimdva2 
 |-  ( O e. V -> ( E. a e. ( ~P O i^i Fin ) ( ( _Ind ` O ) ` a ) = g -> ( g e. ( { 0 , 1 } ^m O ) /\ ( `' g " { 1 } ) e. Fin ) ) )
40 cnvimass 
 |-  ( `' g " { 1 } ) C_ dom g
41 26 biimpa 
 |-  ( ( O e. V /\ g e. ( { 0 , 1 } ^m O ) ) -> g : O --> { 0 , 1 } )
42 41 fdmd 
 |-  ( ( O e. V /\ g e. ( { 0 , 1 } ^m O ) ) -> dom g = O )
43 42 adantrr 
 |-  ( ( O e. V /\ ( g e. ( { 0 , 1 } ^m O ) /\ ( `' g " { 1 } ) e. Fin ) ) -> dom g = O )
44 40 43 sseqtrid 
 |-  ( ( O e. V /\ ( g e. ( { 0 , 1 } ^m O ) /\ ( `' g " { 1 } ) e. Fin ) ) -> ( `' g " { 1 } ) C_ O )
45 simprr 
 |-  ( ( O e. V /\ ( g e. ( { 0 , 1 } ^m O ) /\ ( `' g " { 1 } ) e. Fin ) ) -> ( `' g " { 1 } ) e. Fin )
46 elfpw 
 |-  ( ( `' g " { 1 } ) e. ( ~P O i^i Fin ) <-> ( ( `' g " { 1 } ) C_ O /\ ( `' g " { 1 } ) e. Fin ) )
47 44 45 46 sylanbrc 
 |-  ( ( O e. V /\ ( g e. ( { 0 , 1 } ^m O ) /\ ( `' g " { 1 } ) e. Fin ) ) -> ( `' g " { 1 } ) e. ( ~P O i^i Fin ) )
48 indpreima 
 |-  ( ( O e. V /\ g : O --> { 0 , 1 } ) -> g = ( ( _Ind ` O ) ` ( `' g " { 1 } ) ) )
49 48 eqcomd 
 |-  ( ( O e. V /\ g : O --> { 0 , 1 } ) -> ( ( _Ind ` O ) ` ( `' g " { 1 } ) ) = g )
50 41 49 syldan 
 |-  ( ( O e. V /\ g e. ( { 0 , 1 } ^m O ) ) -> ( ( _Ind ` O ) ` ( `' g " { 1 } ) ) = g )
51 50 adantrr 
 |-  ( ( O e. V /\ ( g e. ( { 0 , 1 } ^m O ) /\ ( `' g " { 1 } ) e. Fin ) ) -> ( ( _Ind ` O ) ` ( `' g " { 1 } ) ) = g )
52 fveqeq2 
 |-  ( a = ( `' g " { 1 } ) -> ( ( ( _Ind ` O ) ` a ) = g <-> ( ( _Ind ` O ) ` ( `' g " { 1 } ) ) = g ) )
53 52 rspcev 
 |-  ( ( ( `' g " { 1 } ) e. ( ~P O i^i Fin ) /\ ( ( _Ind ` O ) ` ( `' g " { 1 } ) ) = g ) -> E. a e. ( ~P O i^i Fin ) ( ( _Ind ` O ) ` a ) = g )
54 47 51 53 syl2anc 
 |-  ( ( O e. V /\ ( g e. ( { 0 , 1 } ^m O ) /\ ( `' g " { 1 } ) e. Fin ) ) -> E. a e. ( ~P O i^i Fin ) ( ( _Ind ` O ) ` a ) = g )
55 54 ex 
 |-  ( O e. V -> ( ( g e. ( { 0 , 1 } ^m O ) /\ ( `' g " { 1 } ) e. Fin ) -> E. a e. ( ~P O i^i Fin ) ( ( _Ind ` O ) ` a ) = g ) )
56 39 55 impbid 
 |-  ( O e. V -> ( E. a e. ( ~P O i^i Fin ) ( ( _Ind ` O ) ` a ) = g <-> ( g e. ( { 0 , 1 } ^m O ) /\ ( `' g " { 1 } ) e. Fin ) ) )
57 1 8 syl 
 |-  ( O e. V -> ( _Ind ` O ) Fn ~P O )
58 fvelimab 
 |-  ( ( ( _Ind ` O ) Fn ~P O /\ ( ~P O i^i Fin ) C_ ~P O ) -> ( g e. ( ( _Ind ` O ) " ( ~P O i^i Fin ) ) <-> E. a e. ( ~P O i^i Fin ) ( ( _Ind ` O ) ` a ) = g ) )
59 57 4 58 sylancl 
 |-  ( O e. V -> ( g e. ( ( _Ind ` O ) " ( ~P O i^i Fin ) ) <-> E. a e. ( ~P O i^i Fin ) ( ( _Ind ` O ) ` a ) = g ) )
60 cnveq 
 |-  ( f = g -> `' f = `' g )
61 60 imaeq1d 
 |-  ( f = g -> ( `' f " { 1 } ) = ( `' g " { 1 } ) )
62 61 eleq1d 
 |-  ( f = g -> ( ( `' f " { 1 } ) e. Fin <-> ( `' g " { 1 } ) e. Fin ) )
63 62 elrab 
 |-  ( g e. { f e. ( { 0 , 1 } ^m O ) | ( `' f " { 1 } ) e. Fin } <-> ( g e. ( { 0 , 1 } ^m O ) /\ ( `' g " { 1 } ) e. Fin ) )
64 63 a1i 
 |-  ( O e. V -> ( g e. { f e. ( { 0 , 1 } ^m O ) | ( `' f " { 1 } ) e. Fin } <-> ( g e. ( { 0 , 1 } ^m O ) /\ ( `' g " { 1 } ) e. Fin ) ) )
65 56 59 64 3bitr4d 
 |-  ( O e. V -> ( g e. ( ( _Ind ` O ) " ( ~P O i^i Fin ) ) <-> g e. { f e. ( { 0 , 1 } ^m O ) | ( `' f " { 1 } ) e. Fin } ) )
66 65 eqrdv 
 |-  ( O e. V -> ( ( _Ind ` O ) " ( ~P O i^i Fin ) ) = { f e. ( { 0 , 1 } ^m O ) | ( `' f " { 1 } ) e. Fin } )
67 12 13 66 f1oeq123d 
 |-  ( O e. V -> ( ( ( _Ind ` O ) |` ( ~P O i^i Fin ) ) : ( ~P O i^i Fin ) -1-1-onto-> ( ( _Ind ` O ) " ( ~P O i^i Fin ) ) <-> ( ( _Ind ` O ) |` Fin ) : ( ~P O i^i Fin ) -1-1-onto-> { f e. ( { 0 , 1 } ^m O ) | ( `' f " { 1 } ) e. Fin } ) )
68 6 67 mpbid 
 |-  ( O e. V -> ( ( _Ind ` O ) |` Fin ) : ( ~P O i^i Fin ) -1-1-onto-> { f e. ( { 0 , 1 } ^m O ) | ( `' f " { 1 } ) e. Fin } )