Metamath Proof Explorer

Theorem pwfi2f1o

Description: The pw2f1o bijection relates finitely supported indicator functions on a two-element set to finite subsets.MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015) (Revised by AV, 14-Jun-2020)

Ref Expression
Hypotheses pwfi2f1o.s 
|- S = { y e. ( 2o ^m A ) | y finSupp (/) }
pwfi2f1o.f 
|- F = ( x e. S |-> ( `' x " { 1o } ) )
Assertion pwfi2f1o 
|- ( A e. V -> F : S -1-1-onto-> ( ~P A i^i Fin ) )

Proof

Step Hyp Ref Expression
1 pwfi2f1o.s 
 |-  S = { y e. ( 2o ^m A ) | y finSupp (/) }
2 pwfi2f1o.f 
 |-  F = ( x e. S |-> ( `' x " { 1o } ) )
3 eqid 
 |-  ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) = ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) )
4 3 pw2f1o2 
 |-  ( A e. V -> ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) : ( 2o ^m A ) -1-1-onto-> ~P A )
5 f1of1 
 |-  ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) : ( 2o ^m A ) -1-1-onto-> ~P A -> ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) : ( 2o ^m A ) -1-1-> ~P A )
6 4 5 syl 
 |-  ( A e. V -> ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) : ( 2o ^m A ) -1-1-> ~P A )
7 ssrab2 
 |-  { y e. ( 2o ^m A ) | y finSupp (/) } C_ ( 2o ^m A )
8 1 7 eqsstri 
 |-  S C_ ( 2o ^m A )
9 f1ores 
 |-  ( ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) : ( 2o ^m A ) -1-1-> ~P A /\ S C_ ( 2o ^m A ) ) -> ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) |` S ) : S -1-1-onto-> ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) " S ) )
10 6 8 9 sylancl 
 |-  ( A e. V -> ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) |` S ) : S -1-1-onto-> ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) " S ) )
11 elmapfun 
 |-  ( y e. ( 2o ^m A ) -> Fun y )
12 id 
 |-  ( y e. ( 2o ^m A ) -> y e. ( 2o ^m A ) )
13 0ex 
 |-  (/) e. _V
14 13 a1i 
 |-  ( y e. ( 2o ^m A ) -> (/) e. _V )
15 11 12 14 3jca 
 |-  ( y e. ( 2o ^m A ) -> ( Fun y /\ y e. ( 2o ^m A ) /\ (/) e. _V ) )
16 15 adantl 
 |-  ( ( A e. V /\ y e. ( 2o ^m A ) ) -> ( Fun y /\ y e. ( 2o ^m A ) /\ (/) e. _V ) )
17 funisfsupp 
 |-  ( ( Fun y /\ y e. ( 2o ^m A ) /\ (/) e. _V ) -> ( y finSupp (/) <-> ( y supp (/) ) e. Fin ) )
18 16 17 syl 
 |-  ( ( A e. V /\ y e. ( 2o ^m A ) ) -> ( y finSupp (/) <-> ( y supp (/) ) e. Fin ) )
19 14 anim2i 
 |-  ( ( A e. V /\ y e. ( 2o ^m A ) ) -> ( A e. V /\ (/) e. _V ) )
20 elmapi 
 |-  ( y e. ( 2o ^m A ) -> y : A --> 2o )
21 20 adantl 
 |-  ( ( A e. V /\ y e. ( 2o ^m A ) ) -> y : A --> 2o )
22 fsuppeq 
 |-  ( ( A e. V /\ (/) e. _V ) -> ( y : A --> 2o -> ( y supp (/) ) = ( `' y " ( 2o \ { (/) } ) ) ) )
23 19 21 22 sylc 
 |-  ( ( A e. V /\ y e. ( 2o ^m A ) ) -> ( y supp (/) ) = ( `' y " ( 2o \ { (/) } ) ) )
24 df-2o 
 |-  2o = suc 1o
25 df-suc 
 |-  suc 1o = ( 1o u. { 1o } )
26 25 equncomi 
 |-  suc 1o = ( { 1o } u. 1o )
27 24 26 eqtri 
 |-  2o = ( { 1o } u. 1o )
28 df1o2 
 |-  1o = { (/) }
29 28 eqcomi 
 |-  { (/) } = 1o
30 27 29 difeq12i 
 |-  ( 2o \ { (/) } ) = ( ( { 1o } u. 1o ) \ 1o )
31 difun2 
 |-  ( ( { 1o } u. 1o ) \ 1o ) = ( { 1o } \ 1o )
32 incom 
 |-  ( { 1o } i^i 1o ) = ( 1o i^i { 1o } )
33 1on 
 |-  1o e. On
34 33 onordi 
 |-  Ord 1o
35 orddisj 
 |-  ( Ord 1o -> ( 1o i^i { 1o } ) = (/) )
36 34 35 ax-mp 
 |-  ( 1o i^i { 1o } ) = (/)
37 32 36 eqtri 
 |-  ( { 1o } i^i 1o ) = (/)
38 disj3 
 |-  ( ( { 1o } i^i 1o ) = (/) <-> { 1o } = ( { 1o } \ 1o ) )
39 37 38 mpbi 
 |-  { 1o } = ( { 1o } \ 1o )
40 31 39 eqtr4i 
 |-  ( ( { 1o } u. 1o ) \ 1o ) = { 1o }
41 30 40 eqtri 
 |-  ( 2o \ { (/) } ) = { 1o }
42 41 imaeq2i 
 |-  ( `' y " ( 2o \ { (/) } ) ) = ( `' y " { 1o } )
43 23 42 eqtrdi 
 |-  ( ( A e. V /\ y e. ( 2o ^m A ) ) -> ( y supp (/) ) = ( `' y " { 1o } ) )
44 43 eleq1d 
 |-  ( ( A e. V /\ y e. ( 2o ^m A ) ) -> ( ( y supp (/) ) e. Fin <-> ( `' y " { 1o } ) e. Fin ) )
45 cnvimass 
 |-  ( `' y " { 1o } ) C_ dom y
46 45 21 fssdm 
 |-  ( ( A e. V /\ y e. ( 2o ^m A ) ) -> ( `' y " { 1o } ) C_ A )
47 46 biantrurd 
 |-  ( ( A e. V /\ y e. ( 2o ^m A ) ) -> ( ( `' y " { 1o } ) e. Fin <-> ( ( `' y " { 1o } ) C_ A /\ ( `' y " { 1o } ) e. Fin ) ) )
48 18 44 47 3bitrd 
 |-  ( ( A e. V /\ y e. ( 2o ^m A ) ) -> ( y finSupp (/) <-> ( ( `' y " { 1o } ) C_ A /\ ( `' y " { 1o } ) e. Fin ) ) )
49 elfpw 
 |-  ( ( `' y " { 1o } ) e. ( ~P A i^i Fin ) <-> ( ( `' y " { 1o } ) C_ A /\ ( `' y " { 1o } ) e. Fin ) )
50 48 49 bitr4di 
 |-  ( ( A e. V /\ y e. ( 2o ^m A ) ) -> ( y finSupp (/) <-> ( `' y " { 1o } ) e. ( ~P A i^i Fin ) ) )
51 50 rabbidva 
 |-  ( A e. V -> { y e. ( 2o ^m A ) | y finSupp (/) } = { y e. ( 2o ^m A ) | ( `' y " { 1o } ) e. ( ~P A i^i Fin ) } )
52 cnveq 
 |-  ( x = y -> `' x = `' y )
53 52 imaeq1d 
 |-  ( x = y -> ( `' x " { 1o } ) = ( `' y " { 1o } ) )
54 53 cbvmptv 
 |-  ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) = ( y e. ( 2o ^m A ) |-> ( `' y " { 1o } ) )
55 54 mptpreima 
 |-  ( `' ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) " ( ~P A i^i Fin ) ) = { y e. ( 2o ^m A ) | ( `' y " { 1o } ) e. ( ~P A i^i Fin ) }
56 51 1 55 3eqtr4g 
 |-  ( A e. V -> S = ( `' ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) " ( ~P A i^i Fin ) ) )
57 56 imaeq2d 
 |-  ( A e. V -> ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) " S ) = ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) " ( `' ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) " ( ~P A i^i Fin ) ) ) )
58 f1ofo 
 |-  ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) : ( 2o ^m A ) -1-1-onto-> ~P A -> ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) : ( 2o ^m A ) -onto-> ~P A )
59 4 58 syl 
 |-  ( A e. V -> ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) : ( 2o ^m A ) -onto-> ~P A )
60 inss1 
 |-  ( ~P A i^i Fin ) C_ ~P A
61 foimacnv 
 |-  ( ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) : ( 2o ^m A ) -onto-> ~P A /\ ( ~P A i^i Fin ) C_ ~P A ) -> ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) " ( `' ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) " ( ~P A i^i Fin ) ) ) = ( ~P A i^i Fin ) )
62 59 60 61 sylancl 
 |-  ( A e. V -> ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) " ( `' ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) " ( ~P A i^i Fin ) ) ) = ( ~P A i^i Fin ) )
63 57 62 eqtrd 
 |-  ( A e. V -> ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) " S ) = ( ~P A i^i Fin ) )
64 f1oeq3 
 |-  ( ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) " S ) = ( ~P A i^i Fin ) -> ( ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) |` S ) : S -1-1-onto-> ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) " S ) <-> ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) |` S ) : S -1-1-onto-> ( ~P A i^i Fin ) ) )
65 63 64 syl 
 |-  ( A e. V -> ( ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) |` S ) : S -1-1-onto-> ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) " S ) <-> ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) |` S ) : S -1-1-onto-> ( ~P A i^i Fin ) ) )
66 resmpt 
 |-  ( S C_ ( 2o ^m A ) -> ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) |` S ) = ( x e. S |-> ( `' x " { 1o } ) ) )
67 8 66 ax-mp 
 |-  ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) |` S ) = ( x e. S |-> ( `' x " { 1o } ) )
68 67 2 eqtr4i 
 |-  ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) |` S ) = F
69 f1oeq1 
 |-  ( ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) |` S ) = F -> ( ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) |` S ) : S -1-1-onto-> ( ~P A i^i Fin ) <-> F : S -1-1-onto-> ( ~P A i^i Fin ) ) )
70 68 69 mp1i 
 |-  ( A e. V -> ( ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) |` S ) : S -1-1-onto-> ( ~P A i^i Fin ) <-> F : S -1-1-onto-> ( ~P A i^i Fin ) ) )
71 65 70 bitrd 
 |-  ( A e. V -> ( ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) |` S ) : S -1-1-onto-> ( ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) ) " S ) <-> F : S -1-1-onto-> ( ~P A i^i Fin ) ) )
72 10 71 mpbid 
 |-  ( A e. V -> F : S -1-1-onto-> ( ~P A i^i Fin ) )