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 ( 𝐴 ≼ ω → ∃ 𝑓 ( 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ∧ ( dom 𝑓 = ℕ ∨ dom 𝑓 = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 f1o0 ⊢ ∅ : ∅ –1-1-onto→ ∅
2 eqidd ⊢ ( 𝐴 = ∅ → ∅ = ∅ )
3 dm0 ⊢ dom ∅ = ∅
4 3 a1i ⊢ ( 𝐴 = ∅ → dom ∅ = ∅ )
5 id ⊢ ( 𝐴 = ∅ → 𝐴 = ∅ )
6 2 4 5 f1oeq123d ⊢ ( 𝐴 = ∅ → ( ∅ : dom ∅ –1-1-onto→ 𝐴 ↔ ∅ : ∅ –1-1-onto→ ∅ ) )
7 1 6 mpbiri ⊢ ( 𝐴 = ∅ → ∅ : dom ∅ –1-1-onto→ 𝐴 )
8 fveq2 ⊢ ( 𝐴 = ∅ → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ∅ ) )
9 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
10 8 9 eqtrdi ⊢ ( 𝐴 = ∅ → ( ♯ ‘ 𝐴 ) = 0 )
11 10 oveq1d ⊢ ( 𝐴 = ∅ → ( ( ♯ ‘ 𝐴 ) + 1 ) = ( 0 + 1 ) )
12 0p1e1 ⊢ ( 0 + 1 ) = 1
13 11 12 eqtrdi ⊢ ( 𝐴 = ∅ → ( ( ♯ ‘ 𝐴 ) + 1 ) = 1 )
14 13 oveq2d ⊢ ( 𝐴 = ∅ → ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) = ( 1 ..^ 1 ) )
15 fzo0 ⊢ ( 1 ..^ 1 ) = ∅
16 14 15 eqtrdi ⊢ ( 𝐴 = ∅ → ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) = ∅ )
17 4 16 eqtr4d ⊢ ( 𝐴 = ∅ → dom ∅ = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) )
18 17 olcd ⊢ ( 𝐴 = ∅ → ( dom ∅ = ℕ ∨ dom ∅ = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) )
19 7 18 jca ⊢ ( 𝐴 = ∅ → ( ∅ : dom ∅ –1-1-onto→ 𝐴 ∧ ( dom ∅ = ℕ ∨ dom ∅ = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) ) )
20 0ex ⊢ ∅ ∈ V
21 id ⊢ ( 𝑓 = ∅ → 𝑓 = ∅ )
22 dmeq ⊢ ( 𝑓 = ∅ → dom 𝑓 = dom ∅ )
23 eqidd ⊢ ( 𝑓 = ∅ → 𝐴 = 𝐴 )
24 21 22 23 f1oeq123d ⊢ ( 𝑓 = ∅ → ( 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ↔ ∅ : dom ∅ –1-1-onto→ 𝐴 ) )
25 22 eqeq1d ⊢ ( 𝑓 = ∅ → ( dom 𝑓 = ℕ ↔ dom ∅ = ℕ ) )
26 22 eqeq1d ⊢ ( 𝑓 = ∅ → ( dom 𝑓 = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ↔ dom ∅ = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) )
27 25 26 orbi12d ⊢ ( 𝑓 = ∅ → ( ( dom 𝑓 = ℕ ∨ dom 𝑓 = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) ↔ ( dom ∅ = ℕ ∨ dom ∅ = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) ) )
28 24 27 anbi12d ⊢ ( 𝑓 = ∅ → ( ( 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ∧ ( dom 𝑓 = ℕ ∨ dom 𝑓 = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) ) ↔ ( ∅ : dom ∅ –1-1-onto→ 𝐴 ∧ ( dom ∅ = ℕ ∨ dom ∅ = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) ) ) )
29 20 28 spcev ⊢ ( ( ∅ : dom ∅ –1-1-onto→ 𝐴 ∧ ( dom ∅ = ℕ ∨ dom ∅ = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) ) → ∃ 𝑓 ( 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ∧ ( dom 𝑓 = ℕ ∨ dom 𝑓 = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) ) )
30 19 29 syl ⊢ ( 𝐴 = ∅ → ∃ 𝑓 ( 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ∧ ( dom 𝑓 = ℕ ∨ dom 𝑓 = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) ) )
31 30 adantl ⊢ ( ( ( 𝐴 ≼ ω ∧ 𝐴 ∈ Fin ) ∧ 𝐴 = ∅ ) → ∃ 𝑓 ( 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ∧ ( dom 𝑓 = ℕ ∨ dom 𝑓 = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) ) )
32 f1odm ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → dom 𝑓 = ( 1 ... ( ♯ ‘ 𝐴 ) ) )
33 32 f1oeq2d ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → ( 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ↔ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) )
34 33 ibir ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 )
35 34 adantl ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 )
36 32 adantl ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → dom 𝑓 = ( 1 ... ( ♯ ‘ 𝐴 ) ) )
37 simpl ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
38 37 nnzd ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( ♯ ‘ 𝐴 ) ∈ ℤ )
39 fzval3 ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℤ → ( 1 ... ( ♯ ‘ 𝐴 ) ) = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) )
40 38 39 syl ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( 1 ... ( ♯ ‘ 𝐴 ) ) = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) )
41 36 40 eqtrd ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → dom 𝑓 = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) )
42 41 olcd ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( dom 𝑓 = ℕ ∨ dom 𝑓 = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) )
43 35 42 jca ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ∧ ( dom 𝑓 = ℕ ∨ dom 𝑓 = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) ) )
44 43 ex ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → ( 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ∧ ( dom 𝑓 = ℕ ∨ dom 𝑓 = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) ) ) )
45 44 eximdv ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → ∃ 𝑓 ( 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ∧ ( dom 𝑓 = ℕ ∨ dom 𝑓 = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) ) ) )
46 45 imp ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ∃ 𝑓 ( 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ∧ ( dom 𝑓 = ℕ ∨ dom 𝑓 = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) ) )
47 46 adantl ⊢ ( ( ( 𝐴 ≼ ω ∧ 𝐴 ∈ Fin ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ∃ 𝑓 ( 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ∧ ( dom 𝑓 = ℕ ∨ dom 𝑓 = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) ) )
48 fz1f1o ⊢ ( 𝐴 ∈ Fin → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) )
49 48 adantl ⊢ ( ( 𝐴 ≼ ω ∧ 𝐴 ∈ Fin ) → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) )
50 31 47 49 mpjaodan ⊢ ( ( 𝐴 ≼ ω ∧ 𝐴 ∈ Fin ) → ∃ 𝑓 ( 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ∧ ( dom 𝑓 = ℕ ∨ dom 𝑓 = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) ) )
51 isfinite ⊢ ( 𝐴 ∈ Fin ↔ 𝐴 ≺ ω )
52 51 notbii ⊢ ( ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ≺ ω )
53 52 biimpi ⊢ ( ¬ 𝐴 ∈ Fin → ¬ 𝐴 ≺ ω )
54 53 anim2i ⊢ ( ( 𝐴 ≼ ω ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ≼ ω ∧ ¬ 𝐴 ≺ ω ) )
55 bren2 ⊢ ( 𝐴 ≈ ω ↔ ( 𝐴 ≼ ω ∧ ¬ 𝐴 ≺ ω ) )
56 54 55 sylibr ⊢ ( ( 𝐴 ≼ ω ∧ ¬ 𝐴 ∈ Fin ) → 𝐴 ≈ ω )
57 nnenom ⊢ ℕ ≈ ω
58 57 ensymi ⊢ ω ≈ ℕ
59 entr ⊢ ( ( 𝐴 ≈ ω ∧ ω ≈ ℕ ) → 𝐴 ≈ ℕ )
60 56 58 59 sylancl ⊢ ( ( 𝐴 ≼ ω ∧ ¬ 𝐴 ∈ Fin ) → 𝐴 ≈ ℕ )
61 bren ⊢ ( 𝐴 ≈ ℕ ↔ ∃ 𝑔 𝑔 : 𝐴 –1-1-onto→ ℕ )
62 60 61 sylib ⊢ ( ( 𝐴 ≼ ω ∧ ¬ 𝐴 ∈ Fin ) → ∃ 𝑔 𝑔 : 𝐴 –1-1-onto→ ℕ )
63 f1oexbi ⊢ ( ∃ 𝑔 𝑔 : 𝐴 –1-1-onto→ ℕ ↔ ∃ 𝑓 𝑓 : ℕ –1-1-onto→ 𝐴 )
64 62 63 sylib ⊢ ( ( 𝐴 ≼ ω ∧ ¬ 𝐴 ∈ Fin ) → ∃ 𝑓 𝑓 : ℕ –1-1-onto→ 𝐴 )
65 f1odm ⊢ ( 𝑓 : ℕ –1-1-onto→ 𝐴 → dom 𝑓 = ℕ )
66 65 f1oeq2d ⊢ ( 𝑓 : ℕ –1-1-onto→ 𝐴 → ( 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ↔ 𝑓 : ℕ –1-1-onto→ 𝐴 ) )
67 66 ibir ⊢ ( 𝑓 : ℕ –1-1-onto→ 𝐴 → 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 )
68 65 orcd ⊢ ( 𝑓 : ℕ –1-1-onto→ 𝐴 → ( dom 𝑓 = ℕ ∨ dom 𝑓 = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) )
69 67 68 jca ⊢ ( 𝑓 : ℕ –1-1-onto→ 𝐴 → ( 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ∧ ( dom 𝑓 = ℕ ∨ dom 𝑓 = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) ) )
70 69 eximi ⊢ ( ∃ 𝑓 𝑓 : ℕ –1-1-onto→ 𝐴 → ∃ 𝑓 ( 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ∧ ( dom 𝑓 = ℕ ∨ dom 𝑓 = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) ) )
71 64 70 syl ⊢ ( ( 𝐴 ≼ ω ∧ ¬ 𝐴 ∈ Fin ) → ∃ 𝑓 ( 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ∧ ( dom 𝑓 = ℕ ∨ dom 𝑓 = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) ) )
72 50 71 pm2.61dan ⊢ ( 𝐴 ≼ ω → ∃ 𝑓 ( 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ∧ ( dom 𝑓 = ℕ ∨ dom 𝑓 = ( 1 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) ) )