Metamath Proof Explorer

Theorem f1ocnt

Description: Given a countable set A , number its elements by providing a one-to-one mapping either with NN or an integer range starting from 1. The domain of the function can then be used with iundisjcnt or iundisj2cnt . (Contributed by Thierry Arnoux, 25-Jul-2020)

Ref Expression
Assertion f1ocnt 
|- ( A ~<_ _om -> E. f ( f : dom f -1-1-onto-> A /\ ( dom f = NN \/ dom f = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 f1o0 
 |-  (/) : (/) -1-1-onto-> (/)
2 eqidd 
 |-  ( A = (/) -> (/) = (/) )
3 dm0 
 |-  dom (/) = (/)
4 3 a1i 
 |-  ( A = (/) -> dom (/) = (/) )
5 id 
 |-  ( A = (/) -> A = (/) )
6 2 4 5 f1oeq123d 
 |-  ( A = (/) -> ( (/) : dom (/) -1-1-onto-> A <-> (/) : (/) -1-1-onto-> (/) ) )
7 1 6 mpbiri 
 |-  ( A = (/) -> (/) : dom (/) -1-1-onto-> A )
8 fveq2 
 |-  ( A = (/) -> ( # ` A ) = ( # ` (/) ) )
9 hash0 
 |-  ( # ` (/) ) = 0
10 8 9 eqtrdi 
 |-  ( A = (/) -> ( # ` A ) = 0 )
11 10 oveq1d 
 |-  ( A = (/) -> ( ( # ` A ) + 1 ) = ( 0 + 1 ) )
12 0p1e1 
 |-  ( 0 + 1 ) = 1
13 11 12 eqtrdi 
 |-  ( A = (/) -> ( ( # ` A ) + 1 ) = 1 )
14 13 oveq2d 
 |-  ( A = (/) -> ( 1 ..^ ( ( # ` A ) + 1 ) ) = ( 1 ..^ 1 ) )
15 fzo0 
 |-  ( 1 ..^ 1 ) = (/)
16 14 15 eqtrdi 
 |-  ( A = (/) -> ( 1 ..^ ( ( # ` A ) + 1 ) ) = (/) )
17 4 16 eqtr4d 
 |-  ( A = (/) -> dom (/) = ( 1 ..^ ( ( # ` A ) + 1 ) ) )
18 17 olcd 
 |-  ( A = (/) -> ( dom (/) = NN \/ dom (/) = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) )
19 7 18 jca 
 |-  ( A = (/) -> ( (/) : dom (/) -1-1-onto-> A /\ ( dom (/) = NN \/ dom (/) = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) ) )
20 0ex 
 |-  (/) e. _V
21 id 
 |-  ( f = (/) -> f = (/) )
22 dmeq 
 |-  ( f = (/) -> dom f = dom (/) )
23 eqidd 
 |-  ( f = (/) -> A = A )
24 21 22 23 f1oeq123d 
 |-  ( f = (/) -> ( f : dom f -1-1-onto-> A <-> (/) : dom (/) -1-1-onto-> A ) )
25 22 eqeq1d 
 |-  ( f = (/) -> ( dom f = NN <-> dom (/) = NN ) )
26 22 eqeq1d 
 |-  ( f = (/) -> ( dom f = ( 1 ..^ ( ( # ` A ) + 1 ) ) <-> dom (/) = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) )
27 25 26 orbi12d 
 |-  ( f = (/) -> ( ( dom f = NN \/ dom f = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) <-> ( dom (/) = NN \/ dom (/) = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) ) )
28 24 27 anbi12d 
 |-  ( f = (/) -> ( ( f : dom f -1-1-onto-> A /\ ( dom f = NN \/ dom f = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) ) <-> ( (/) : dom (/) -1-1-onto-> A /\ ( dom (/) = NN \/ dom (/) = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) ) ) )
29 20 28 spcev 
 |-  ( ( (/) : dom (/) -1-1-onto-> A /\ ( dom (/) = NN \/ dom (/) = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) ) -> E. f ( f : dom f -1-1-onto-> A /\ ( dom f = NN \/ dom f = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) ) )
30 19 29 syl 
 |-  ( A = (/) -> E. f ( f : dom f -1-1-onto-> A /\ ( dom f = NN \/ dom f = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) ) )
31 30 adantl 
 |-  ( ( ( A ~<_ _om /\ A e. Fin ) /\ A = (/) ) -> E. f ( f : dom f -1-1-onto-> A /\ ( dom f = NN \/ dom f = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) ) )
32 f1odm 
 |-  ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> dom f = ( 1 ... ( # ` A ) ) )
33 32 f1oeq2d 
 |-  ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> ( f : dom f -1-1-onto-> A <-> f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) )
34 33 ibir 
 |-  ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> f : dom f -1-1-onto-> A )
35 34 adantl 
 |-  ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> f : dom f -1-1-onto-> A )
36 32 adantl 
 |-  ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> dom f = ( 1 ... ( # ` A ) ) )
37 simpl 
 |-  ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( # ` A ) e. NN )
38 37 nnzd 
 |-  ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( # ` A ) e. ZZ )
39 fzval3 
 |-  ( ( # ` A ) e. ZZ -> ( 1 ... ( # ` A ) ) = ( 1 ..^ ( ( # ` A ) + 1 ) ) )
40 38 39 syl 
 |-  ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( 1 ... ( # ` A ) ) = ( 1 ..^ ( ( # ` A ) + 1 ) ) )
41 36 40 eqtrd 
 |-  ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> dom f = ( 1 ..^ ( ( # ` A ) + 1 ) ) )
42 41 olcd 
 |-  ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( dom f = NN \/ dom f = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) )
43 35 42 jca 
 |-  ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( f : dom f -1-1-onto-> A /\ ( dom f = NN \/ dom f = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) ) )
44 43 ex 
 |-  ( ( # ` A ) e. NN -> ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> ( f : dom f -1-1-onto-> A /\ ( dom f = NN \/ dom f = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) ) ) )
45 44 eximdv 
 |-  ( ( # ` A ) e. NN -> ( E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> E. f ( f : dom f -1-1-onto-> A /\ ( dom f = NN \/ dom f = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) ) ) )
46 45 imp 
 |-  ( ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> E. f ( f : dom f -1-1-onto-> A /\ ( dom f = NN \/ dom f = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) ) )
47 46 adantl 
 |-  ( ( ( A ~<_ _om /\ A e. Fin ) /\ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> E. f ( f : dom f -1-1-onto-> A /\ ( dom f = NN \/ dom f = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) ) )
48 fz1f1o 
 |-  ( A e. Fin -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
49 48 adantl 
 |-  ( ( A ~<_ _om /\ A e. Fin ) -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
50 31 47 49 mpjaodan 
 |-  ( ( A ~<_ _om /\ A e. Fin ) -> E. f ( f : dom f -1-1-onto-> A /\ ( dom f = NN \/ dom f = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) ) )
51 isfinite 
 |-  ( A e. Fin <-> A ~< _om )
52 51 notbii 
 |-  ( -. A e. Fin <-> -. A ~< _om )
53 52 biimpi 
 |-  ( -. A e. Fin -> -. A ~< _om )
54 53 anim2i 
 |-  ( ( A ~<_ _om /\ -. A e. Fin ) -> ( A ~<_ _om /\ -. A ~< _om ) )
55 bren2 
 |-  ( A ~~ _om <-> ( A ~<_ _om /\ -. A ~< _om ) )
56 54 55 sylibr 
 |-  ( ( A ~<_ _om /\ -. A e. Fin ) -> A ~~ _om )
57 nnenom 
 |-  NN ~~ _om
58 57 ensymi 
 |-  _om ~~ NN
59 entr 
 |-  ( ( A ~~ _om /\ _om ~~ NN ) -> A ~~ NN )
60 56 58 59 sylancl 
 |-  ( ( A ~<_ _om /\ -. A e. Fin ) -> A ~~ NN )
61 bren 
 |-  ( A ~~ NN <-> E. g g : A -1-1-onto-> NN )
62 60 61 sylib 
 |-  ( ( A ~<_ _om /\ -. A e. Fin ) -> E. g g : A -1-1-onto-> NN )
63 f1oexbi 
 |-  ( E. g g : A -1-1-onto-> NN <-> E. f f : NN -1-1-onto-> A )
64 62 63 sylib 
 |-  ( ( A ~<_ _om /\ -. A e. Fin ) -> E. f f : NN -1-1-onto-> A )
65 f1odm 
 |-  ( f : NN -1-1-onto-> A -> dom f = NN )
66 65 f1oeq2d 
 |-  ( f : NN -1-1-onto-> A -> ( f : dom f -1-1-onto-> A <-> f : NN -1-1-onto-> A ) )
67 66 ibir 
 |-  ( f : NN -1-1-onto-> A -> f : dom f -1-1-onto-> A )
68 65 orcd 
 |-  ( f : NN -1-1-onto-> A -> ( dom f = NN \/ dom f = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) )
69 67 68 jca 
 |-  ( f : NN -1-1-onto-> A -> ( f : dom f -1-1-onto-> A /\ ( dom f = NN \/ dom f = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) ) )
70 69 eximi 
 |-  ( E. f f : NN -1-1-onto-> A -> E. f ( f : dom f -1-1-onto-> A /\ ( dom f = NN \/ dom f = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) ) )
71 64 70 syl 
 |-  ( ( A ~<_ _om /\ -. A e. Fin ) -> E. f ( f : dom f -1-1-onto-> A /\ ( dom f = NN \/ dom f = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) ) )
72 50 71 pm2.61dan 
 |-  ( A ~<_ _om -> E. f ( f : dom f -1-1-onto-> A /\ ( dom f = NN \/ dom f = ( 1 ..^ ( ( # ` A ) + 1 ) ) ) ) )