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 ( 𝑂𝑉 → ( ( 𝟭 ‘ 𝑂 ) ↾ Fin ) : ( 𝒫 𝑂 ∩ Fin ) –1-1-onto→ { 𝑓 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∣ ( 𝑓 “ { 1 } ) ∈ Fin } )

Proof

Step Hyp Ref Expression
1 indf1o ( 𝑂𝑉 → ( 𝟭 ‘ 𝑂 ) : 𝒫 𝑂1-1-onto→ ( { 0 , 1 } ↑m 𝑂 ) )
2 f1of1 ( ( 𝟭 ‘ 𝑂 ) : 𝒫 𝑂1-1-onto→ ( { 0 , 1 } ↑m 𝑂 ) → ( 𝟭 ‘ 𝑂 ) : 𝒫 𝑂1-1→ ( { 0 , 1 } ↑m 𝑂 ) )
3 1 2 syl ( 𝑂𝑉 → ( 𝟭 ‘ 𝑂 ) : 𝒫 𝑂1-1→ ( { 0 , 1 } ↑m 𝑂 ) )
4 inss1 ( 𝒫 𝑂 ∩ Fin ) ⊆ 𝒫 𝑂
5 f1ores ( ( ( 𝟭 ‘ 𝑂 ) : 𝒫 𝑂1-1→ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( 𝒫 𝑂 ∩ Fin ) ⊆ 𝒫 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ↾ ( 𝒫 𝑂 ∩ Fin ) ) : ( 𝒫 𝑂 ∩ Fin ) –1-1-onto→ ( ( 𝟭 ‘ 𝑂 ) “ ( 𝒫 𝑂 ∩ Fin ) ) )
6 3 4 5 sylancl ( 𝑂𝑉 → ( ( 𝟭 ‘ 𝑂 ) ↾ ( 𝒫 𝑂 ∩ Fin ) ) : ( 𝒫 𝑂 ∩ Fin ) –1-1-onto→ ( ( 𝟭 ‘ 𝑂 ) “ ( 𝒫 𝑂 ∩ Fin ) ) )
7 resres ( ( ( 𝟭 ‘ 𝑂 ) ↾ 𝒫 𝑂 ) ↾ Fin ) = ( ( 𝟭 ‘ 𝑂 ) ↾ ( 𝒫 𝑂 ∩ Fin ) )
8 f1ofn ( ( 𝟭 ‘ 𝑂 ) : 𝒫 𝑂1-1-onto→ ( { 0 , 1 } ↑m 𝑂 ) → ( 𝟭 ‘ 𝑂 ) Fn 𝒫 𝑂 )
9 fnresdm ( ( 𝟭 ‘ 𝑂 ) Fn 𝒫 𝑂 → ( ( 𝟭 ‘ 𝑂 ) ↾ 𝒫 𝑂 ) = ( 𝟭 ‘ 𝑂 ) )
10 1 8 9 3syl ( 𝑂𝑉 → ( ( 𝟭 ‘ 𝑂 ) ↾ 𝒫 𝑂 ) = ( 𝟭 ‘ 𝑂 ) )
11 10 reseq1d ( 𝑂𝑉 → ( ( ( 𝟭 ‘ 𝑂 ) ↾ 𝒫 𝑂 ) ↾ Fin ) = ( ( 𝟭 ‘ 𝑂 ) ↾ Fin ) )
12 7 11 eqtr3id ( 𝑂𝑉 → ( ( 𝟭 ‘ 𝑂 ) ↾ ( 𝒫 𝑂 ∩ Fin ) ) = ( ( 𝟭 ‘ 𝑂 ) ↾ Fin ) )
13 eqidd ( 𝑂𝑉 → ( 𝒫 𝑂 ∩ Fin ) = ( 𝒫 𝑂 ∩ Fin ) )
14 simpll ( ( ( 𝑂𝑉𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) → 𝑂𝑉 )
15 simpr ( ( 𝑂𝑉𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) → 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) )
16 4 15 sselid ( ( 𝑂𝑉𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) → 𝑎 ∈ 𝒫 𝑂 )
17 16 elpwid ( ( 𝑂𝑉𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) → 𝑎𝑂 )
18 indf ( ( 𝑂𝑉𝑎𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) : 𝑂 ⟶ { 0 , 1 } )
19 17 18 syldan ( ( 𝑂𝑉𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) : 𝑂 ⟶ { 0 , 1 } )
20 19 adantr ( ( ( 𝑂𝑉𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) : 𝑂 ⟶ { 0 , 1 } )
21 simpr ( ( ( 𝑂𝑉𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 )
22 21 feq1d ( ( ( 𝑂𝑉𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) : 𝑂 ⟶ { 0 , 1 } ↔ 𝑔 : 𝑂 ⟶ { 0 , 1 } ) )
23 20 22 mpbid ( ( ( 𝑂𝑉𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) → 𝑔 : 𝑂 ⟶ { 0 , 1 } )
24 prex { 0 , 1 } ∈ V
25 elmapg ( ( { 0 , 1 } ∈ V ∧ 𝑂𝑉 ) → ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ↔ 𝑔 : 𝑂 ⟶ { 0 , 1 } ) )
26 24 25 mpan ( 𝑂𝑉 → ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ↔ 𝑔 : 𝑂 ⟶ { 0 , 1 } ) )
27 26 biimpar ( ( 𝑂𝑉𝑔 : 𝑂 ⟶ { 0 , 1 } ) → 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) )
28 14 23 27 syl2anc ( ( ( 𝑂𝑉𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) → 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) )
29 21 cnveqd ( ( ( 𝑂𝑉𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 )
30 29 imaeq1d ( ( ( 𝑂𝑉𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) “ { 1 } ) = ( 𝑔 “ { 1 } ) )
31 indpi1 ( ( 𝑂𝑉𝑎𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) “ { 1 } ) = 𝑎 )
32 17 31 syldan ( ( 𝑂𝑉𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) “ { 1 } ) = 𝑎 )
33 inss2 ( 𝒫 𝑂 ∩ Fin ) ⊆ Fin
34 33 15 sselid ( ( 𝑂𝑉𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) → 𝑎 ∈ Fin )
35 32 34 eqeltrd ( ( 𝑂𝑉𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) “ { 1 } ) ∈ Fin )
36 35 adantr ( ( ( 𝑂𝑉𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) “ { 1 } ) ∈ Fin )
37 30 36 eqeltrrd ( ( ( 𝑂𝑉𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) → ( 𝑔 “ { 1 } ) ∈ Fin )
38 28 37 jca ( ( ( 𝑂𝑉𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) → ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( 𝑔 “ { 1 } ) ∈ Fin ) )
39 38 rexlimdva2 ( 𝑂𝑉 → ( ∃ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 → ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( 𝑔 “ { 1 } ) ∈ Fin ) ) )
40 cnvimass ( 𝑔 “ { 1 } ) ⊆ dom 𝑔
41 26 biimpa ( ( 𝑂𝑉𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ) → 𝑔 : 𝑂 ⟶ { 0 , 1 } )
42 41 fdmd ( ( 𝑂𝑉𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ) → dom 𝑔 = 𝑂 )
43 42 adantrr ( ( 𝑂𝑉 ∧ ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( 𝑔 “ { 1 } ) ∈ Fin ) ) → dom 𝑔 = 𝑂 )
44 40 43 sseqtrid ( ( 𝑂𝑉 ∧ ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( 𝑔 “ { 1 } ) ∈ Fin ) ) → ( 𝑔 “ { 1 } ) ⊆ 𝑂 )
45 simprr ( ( 𝑂𝑉 ∧ ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( 𝑔 “ { 1 } ) ∈ Fin ) ) → ( 𝑔 “ { 1 } ) ∈ Fin )
46 elfpw ( ( 𝑔 “ { 1 } ) ∈ ( 𝒫 𝑂 ∩ Fin ) ↔ ( ( 𝑔 “ { 1 } ) ⊆ 𝑂 ∧ ( 𝑔 “ { 1 } ) ∈ Fin ) )
47 44 45 46 sylanbrc ( ( 𝑂𝑉 ∧ ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( 𝑔 “ { 1 } ) ∈ Fin ) ) → ( 𝑔 “ { 1 } ) ∈ ( 𝒫 𝑂 ∩ Fin ) )
48 indpreima ( ( 𝑂𝑉𝑔 : 𝑂 ⟶ { 0 , 1 } ) → 𝑔 = ( ( 𝟭 ‘ 𝑂 ) ‘ ( 𝑔 “ { 1 } ) ) )
49 48 eqcomd ( ( 𝑂𝑉𝑔 : 𝑂 ⟶ { 0 , 1 } ) → ( ( 𝟭 ‘ 𝑂 ) ‘ ( 𝑔 “ { 1 } ) ) = 𝑔 )
50 41 49 syldan ( ( 𝑂𝑉𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ) → ( ( 𝟭 ‘ 𝑂 ) ‘ ( 𝑔 “ { 1 } ) ) = 𝑔 )
51 50 adantrr ( ( 𝑂𝑉 ∧ ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( 𝑔 “ { 1 } ) ∈ Fin ) ) → ( ( 𝟭 ‘ 𝑂 ) ‘ ( 𝑔 “ { 1 } ) ) = 𝑔 )
52 fveqeq2 ( 𝑎 = ( 𝑔 “ { 1 } ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ↔ ( ( 𝟭 ‘ 𝑂 ) ‘ ( 𝑔 “ { 1 } ) ) = 𝑔 ) )
53 52 rspcev ( ( ( 𝑔 “ { 1 } ) ∈ ( 𝒫 𝑂 ∩ Fin ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ ( 𝑔 “ { 1 } ) ) = 𝑔 ) → ∃ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 )
54 47 51 53 syl2anc ( ( 𝑂𝑉 ∧ ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( 𝑔 “ { 1 } ) ∈ Fin ) ) → ∃ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 )
55 54 ex ( 𝑂𝑉 → ( ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( 𝑔 “ { 1 } ) ∈ Fin ) → ∃ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) )
56 39 55 impbid ( 𝑂𝑉 → ( ∃ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ↔ ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( 𝑔 “ { 1 } ) ∈ Fin ) ) )
57 1 8 syl ( 𝑂𝑉 → ( 𝟭 ‘ 𝑂 ) Fn 𝒫 𝑂 )
58 fvelimab ( ( ( 𝟭 ‘ 𝑂 ) Fn 𝒫 𝑂 ∧ ( 𝒫 𝑂 ∩ Fin ) ⊆ 𝒫 𝑂 ) → ( 𝑔 ∈ ( ( 𝟭 ‘ 𝑂 ) “ ( 𝒫 𝑂 ∩ Fin ) ) ↔ ∃ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) )
59 57 4 58 sylancl ( 𝑂𝑉 → ( 𝑔 ∈ ( ( 𝟭 ‘ 𝑂 ) “ ( 𝒫 𝑂 ∩ Fin ) ) ↔ ∃ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) )
60 cnveq ( 𝑓 = 𝑔 𝑓 = 𝑔 )
61 60 imaeq1d ( 𝑓 = 𝑔 → ( 𝑓 “ { 1 } ) = ( 𝑔 “ { 1 } ) )
62 61 eleq1d ( 𝑓 = 𝑔 → ( ( 𝑓 “ { 1 } ) ∈ Fin ↔ ( 𝑔 “ { 1 } ) ∈ Fin ) )
63 62 elrab ( 𝑔 ∈ { 𝑓 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∣ ( 𝑓 “ { 1 } ) ∈ Fin } ↔ ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( 𝑔 “ { 1 } ) ∈ Fin ) )
64 63 a1i ( 𝑂𝑉 → ( 𝑔 ∈ { 𝑓 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∣ ( 𝑓 “ { 1 } ) ∈ Fin } ↔ ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( 𝑔 “ { 1 } ) ∈ Fin ) ) )
65 56 59 64 3bitr4d ( 𝑂𝑉 → ( 𝑔 ∈ ( ( 𝟭 ‘ 𝑂 ) “ ( 𝒫 𝑂 ∩ Fin ) ) ↔ 𝑔 ∈ { 𝑓 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∣ ( 𝑓 “ { 1 } ) ∈ Fin } ) )
66 65 eqrdv ( 𝑂𝑉 → ( ( 𝟭 ‘ 𝑂 ) “ ( 𝒫 𝑂 ∩ Fin ) ) = { 𝑓 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∣ ( 𝑓 “ { 1 } ) ∈ Fin } )
67 12 13 66 f1oeq123d ( 𝑂𝑉 → ( ( ( 𝟭 ‘ 𝑂 ) ↾ ( 𝒫 𝑂 ∩ Fin ) ) : ( 𝒫 𝑂 ∩ Fin ) –1-1-onto→ ( ( 𝟭 ‘ 𝑂 ) “ ( 𝒫 𝑂 ∩ Fin ) ) ↔ ( ( 𝟭 ‘ 𝑂 ) ↾ Fin ) : ( 𝒫 𝑂 ∩ Fin ) –1-1-onto→ { 𝑓 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∣ ( 𝑓 “ { 1 } ) ∈ Fin } ) )
68 6 67 mpbid ( 𝑂𝑉 → ( ( 𝟭 ‘ 𝑂 ) ↾ Fin ) : ( 𝒫 𝑂 ∩ Fin ) –1-1-onto→ { 𝑓 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∣ ( 𝑓 “ { 1 } ) ∈ Fin } )