Step | Hyp | Ref
| Expression |
1 | | f1o0 6173 |
. . . . . . 7
⊢
∅:∅–1-1-onto→∅ |
2 | | eqidd 2623 |
. . . . . . . 8
⊢ (𝐴 = ∅ → ∅ =
∅) |
3 | | dm0 5339 |
. . . . . . . . 9
⊢ dom
∅ = ∅ |
4 | 3 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 = ∅ → dom ∅ =
∅) |
5 | | id 22 |
. . . . . . . 8
⊢ (𝐴 = ∅ → 𝐴 = ∅) |
6 | 2, 4, 5 | f1oeq123d 6133 |
. . . . . . 7
⊢ (𝐴 = ∅ → (∅:dom
∅–1-1-onto→𝐴 ↔ ∅:∅–1-1-onto→∅)) |
7 | 1, 6 | mpbiri 248 |
. . . . . 6
⊢ (𝐴 = ∅ → ∅:dom
∅–1-1-onto→𝐴) |
8 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝐴 = ∅ → (#‘𝐴) =
(#‘∅)) |
9 | | hash0 13158 |
. . . . . . . . . . . . 13
⊢
(#‘∅) = 0 |
10 | 8, 9 | syl6eq 2672 |
. . . . . . . . . . . 12
⊢ (𝐴 = ∅ → (#‘𝐴) = 0) |
11 | 10 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝐴 = ∅ →
((#‘𝐴) + 1) = (0 +
1)) |
12 | | 0p1e1 11132 |
. . . . . . . . . . 11
⊢ (0 + 1) =
1 |
13 | 11, 12 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (𝐴 = ∅ →
((#‘𝐴) + 1) =
1) |
14 | 13 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝐴 = ∅ →
(1..^((#‘𝐴) + 1)) =
(1..^1)) |
15 | | fzo0 12492 |
. . . . . . . . 9
⊢ (1..^1) =
∅ |
16 | 14, 15 | syl6eq 2672 |
. . . . . . . 8
⊢ (𝐴 = ∅ →
(1..^((#‘𝐴) + 1)) =
∅) |
17 | 4, 16 | eqtr4d 2659 |
. . . . . . 7
⊢ (𝐴 = ∅ → dom ∅ =
(1..^((#‘𝐴) +
1))) |
18 | 17 | olcd 408 |
. . . . . 6
⊢ (𝐴 = ∅ → (dom ∅ =
ℕ ∨ dom ∅ = (1..^((#‘𝐴) + 1)))) |
19 | 7, 18 | jca 554 |
. . . . 5
⊢ (𝐴 = ∅ → (∅:dom
∅–1-1-onto→𝐴 ∧ (dom ∅ = ℕ ∨ dom
∅ = (1..^((#‘𝐴)
+ 1))))) |
20 | | 0ex 4790 |
. . . . . 6
⊢ ∅
∈ V |
21 | | id 22 |
. . . . . . . 8
⊢ (𝑓 = ∅ → 𝑓 = ∅) |
22 | | dmeq 5324 |
. . . . . . . 8
⊢ (𝑓 = ∅ → dom 𝑓 = dom ∅) |
23 | | eqidd 2623 |
. . . . . . . 8
⊢ (𝑓 = ∅ → 𝐴 = 𝐴) |
24 | 21, 22, 23 | f1oeq123d 6133 |
. . . . . . 7
⊢ (𝑓 = ∅ → (𝑓:dom 𝑓–1-1-onto→𝐴 ↔ ∅:dom
∅–1-1-onto→𝐴)) |
25 | 22 | eqeq1d 2624 |
. . . . . . . 8
⊢ (𝑓 = ∅ → (dom 𝑓 = ℕ ↔ dom ∅ =
ℕ)) |
26 | 22 | eqeq1d 2624 |
. . . . . . . 8
⊢ (𝑓 = ∅ → (dom 𝑓 = (1..^((#‘𝐴) + 1)) ↔ dom ∅ =
(1..^((#‘𝐴) +
1)))) |
27 | 25, 26 | orbi12d 746 |
. . . . . . 7
⊢ (𝑓 = ∅ → ((dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((#‘𝐴) + 1))) ↔ (dom ∅ =
ℕ ∨ dom ∅ = (1..^((#‘𝐴) + 1))))) |
28 | 24, 27 | anbi12d 747 |
. . . . . 6
⊢ (𝑓 = ∅ → ((𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((#‘𝐴) + 1)))) ↔ (∅:dom
∅–1-1-onto→𝐴 ∧ (dom ∅ = ℕ ∨ dom
∅ = (1..^((#‘𝐴)
+ 1)))))) |
29 | 20, 28 | spcev 3300 |
. . . . 5
⊢
((∅:dom ∅–1-1-onto→𝐴 ∧ (dom ∅ = ℕ
∨ dom ∅ = (1..^((#‘𝐴) + 1)))) → ∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((#‘𝐴) + 1))))) |
30 | 19, 29 | syl 17 |
. . . 4
⊢ (𝐴 = ∅ → ∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((#‘𝐴) + 1))))) |
31 | 30 | adantl 482 |
. . 3
⊢ (((𝐴 ≼ ω ∧ 𝐴 ∈ Fin) ∧ 𝐴 = ∅) → ∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((#‘𝐴) + 1))))) |
32 | | f1odm 6141 |
. . . . . . . . . . 11
⊢ (𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → dom 𝑓 = (1...(#‘𝐴))) |
33 | | f1oeq2 6128 |
. . . . . . . . . . 11
⊢ (dom
𝑓 = (1...(#‘𝐴)) → (𝑓:dom 𝑓–1-1-onto→𝐴 ↔ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) |
34 | 32, 33 | syl 17 |
. . . . . . . . . 10
⊢ (𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → (𝑓:dom 𝑓–1-1-onto→𝐴 ↔ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) |
35 | 34 | ibir 257 |
. . . . . . . . 9
⊢ (𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → 𝑓:dom 𝑓–1-1-onto→𝐴) |
36 | 35 | adantl 482 |
. . . . . . . 8
⊢
(((#‘𝐴) ∈
ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) → 𝑓:dom 𝑓–1-1-onto→𝐴) |
37 | 32 | adantl 482 |
. . . . . . . . . 10
⊢
(((#‘𝐴) ∈
ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) → dom 𝑓 = (1...(#‘𝐴))) |
38 | | simpl 473 |
. . . . . . . . . . . 12
⊢
(((#‘𝐴) ∈
ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) → (#‘𝐴) ∈
ℕ) |
39 | 38 | nnzd 11481 |
. . . . . . . . . . 11
⊢
(((#‘𝐴) ∈
ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) → (#‘𝐴) ∈
ℤ) |
40 | | fzval3 12536 |
. . . . . . . . . . 11
⊢
((#‘𝐴) ∈
ℤ → (1...(#‘𝐴)) = (1..^((#‘𝐴) + 1))) |
41 | 39, 40 | syl 17 |
. . . . . . . . . 10
⊢
(((#‘𝐴) ∈
ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) → (1...(#‘𝐴)) = (1..^((#‘𝐴) + 1))) |
42 | 37, 41 | eqtrd 2656 |
. . . . . . . . 9
⊢
(((#‘𝐴) ∈
ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) → dom 𝑓 = (1..^((#‘𝐴) + 1))) |
43 | 42 | olcd 408 |
. . . . . . . 8
⊢
(((#‘𝐴) ∈
ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) → (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((#‘𝐴) + 1)))) |
44 | 36, 43 | jca 554 |
. . . . . . 7
⊢
(((#‘𝐴) ∈
ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) → (𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((#‘𝐴) + 1))))) |
45 | 44 | ex 450 |
. . . . . 6
⊢
((#‘𝐴) ∈
ℕ → (𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → (𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((#‘𝐴) + 1)))))) |
46 | 45 | eximdv 1846 |
. . . . 5
⊢
((#‘𝐴) ∈
ℕ → (∃𝑓
𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → ∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((#‘𝐴) + 1)))))) |
47 | 46 | imp 445 |
. . . 4
⊢
(((#‘𝐴) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) → ∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((#‘𝐴) + 1))))) |
48 | 47 | adantl 482 |
. . 3
⊢ (((𝐴 ≼ ω ∧ 𝐴 ∈ Fin) ∧
((#‘𝐴) ∈ ℕ
∧ ∃𝑓 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → ∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((#‘𝐴) + 1))))) |
49 | | fz1f1o 14441 |
. . . 4
⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨ ((#‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴))) |
50 | 49 | adantl 482 |
. . 3
⊢ ((𝐴 ≼ ω ∧ 𝐴 ∈ Fin) → (𝐴 = ∅ ∨ ((#‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴))) |
51 | 31, 48, 50 | mpjaodan 827 |
. 2
⊢ ((𝐴 ≼ ω ∧ 𝐴 ∈ Fin) → ∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((#‘𝐴) + 1))))) |
52 | | isfinite 8549 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Fin ↔ 𝐴 ≺
ω) |
53 | 52 | notbii 310 |
. . . . . . . . 9
⊢ (¬
𝐴 ∈ Fin ↔ ¬
𝐴 ≺
ω) |
54 | 53 | biimpi 206 |
. . . . . . . 8
⊢ (¬
𝐴 ∈ Fin → ¬
𝐴 ≺
ω) |
55 | 54 | anim2i 593 |
. . . . . . 7
⊢ ((𝐴 ≼ ω ∧ ¬
𝐴 ∈ Fin) → (𝐴 ≼ ω ∧ ¬
𝐴 ≺
ω)) |
56 | | bren2 7986 |
. . . . . . 7
⊢ (𝐴 ≈ ω ↔ (𝐴 ≼ ω ∧ ¬
𝐴 ≺
ω)) |
57 | 55, 56 | sylibr 224 |
. . . . . 6
⊢ ((𝐴 ≼ ω ∧ ¬
𝐴 ∈ Fin) → 𝐴 ≈
ω) |
58 | | nnenom 12779 |
. . . . . . 7
⊢ ℕ
≈ ω |
59 | 58 | ensymi 8006 |
. . . . . 6
⊢ ω
≈ ℕ |
60 | | entr 8008 |
. . . . . 6
⊢ ((𝐴 ≈ ω ∧ ω
≈ ℕ) → 𝐴
≈ ℕ) |
61 | 57, 59, 60 | sylancl 694 |
. . . . 5
⊢ ((𝐴 ≼ ω ∧ ¬
𝐴 ∈ Fin) → 𝐴 ≈
ℕ) |
62 | | bren 7964 |
. . . . 5
⊢ (𝐴 ≈ ℕ ↔
∃𝑔 𝑔:𝐴–1-1-onto→ℕ) |
63 | 61, 62 | sylib 208 |
. . . 4
⊢ ((𝐴 ≼ ω ∧ ¬
𝐴 ∈ Fin) →
∃𝑔 𝑔:𝐴–1-1-onto→ℕ) |
64 | | f1oexbi 7116 |
. . . 4
⊢
(∃𝑔 𝑔:𝐴–1-1-onto→ℕ ↔ ∃𝑓 𝑓:ℕ–1-1-onto→𝐴) |
65 | 63, 64 | sylib 208 |
. . 3
⊢ ((𝐴 ≼ ω ∧ ¬
𝐴 ∈ Fin) →
∃𝑓 𝑓:ℕ–1-1-onto→𝐴) |
66 | | f1odm 6141 |
. . . . . . 7
⊢ (𝑓:ℕ–1-1-onto→𝐴 → dom 𝑓 = ℕ) |
67 | | f1oeq2 6128 |
. . . . . . 7
⊢ (dom
𝑓 = ℕ → (𝑓:dom 𝑓–1-1-onto→𝐴 ↔ 𝑓:ℕ–1-1-onto→𝐴)) |
68 | 66, 67 | syl 17 |
. . . . . 6
⊢ (𝑓:ℕ–1-1-onto→𝐴 → (𝑓:dom 𝑓–1-1-onto→𝐴 ↔ 𝑓:ℕ–1-1-onto→𝐴)) |
69 | 68 | ibir 257 |
. . . . 5
⊢ (𝑓:ℕ–1-1-onto→𝐴 → 𝑓:dom 𝑓–1-1-onto→𝐴) |
70 | 66 | orcd 407 |
. . . . 5
⊢ (𝑓:ℕ–1-1-onto→𝐴 → (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((#‘𝐴) + 1)))) |
71 | 69, 70 | jca 554 |
. . . 4
⊢ (𝑓:ℕ–1-1-onto→𝐴 → (𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((#‘𝐴) + 1))))) |
72 | 71 | eximi 1762 |
. . 3
⊢
(∃𝑓 𝑓:ℕ–1-1-onto→𝐴 → ∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((#‘𝐴) + 1))))) |
73 | 65, 72 | syl 17 |
. 2
⊢ ((𝐴 ≼ ω ∧ ¬
𝐴 ∈ Fin) →
∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((#‘𝐴) + 1))))) |
74 | 51, 73 | pm2.61dan 832 |
1
⊢ (𝐴 ≼ ω →
∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((#‘𝐴) + 1))))) |