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 sseldi ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑎 ∈ ( 𝒫 𝑂 ∩ 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 sseldi ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑎 ∈ ( 𝒫 𝑂 ∩ 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 } )