Step | Hyp | Ref
| Expression |
1 | | f1o0 6719 |
. . . . . . 7
⊢
∅:∅–1-1-onto→∅ |
2 | | eqidd 2740 |
. . . . . . . 8
⊢ (𝐴 = ∅ → ∅ =
∅) |
3 | | dm0 5807 |
. . . . . . . . 9
⊢ dom
∅ = ∅ |
4 | 3 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 = ∅ → dom ∅ =
∅) |
5 | | id 22 |
. . . . . . . 8
⊢ (𝐴 = ∅ → 𝐴 = ∅) |
6 | 2, 4, 5 | f1oeq123d 6677 |
. . . . . . 7
⊢ (𝐴 = ∅ → (∅:dom
∅–1-1-onto→𝐴 ↔ ∅:∅–1-1-onto→∅)) |
7 | 1, 6 | mpbiri 261 |
. . . . . 6
⊢ (𝐴 = ∅ → ∅:dom
∅–1-1-onto→𝐴) |
8 | | fveq2 6739 |
. . . . . . . . . . . . 13
⊢ (𝐴 = ∅ →
(♯‘𝐴) =
(♯‘∅)) |
9 | | hash0 13967 |
. . . . . . . . . . . . 13
⊢
(♯‘∅) = 0 |
10 | 8, 9 | eqtrdi 2796 |
. . . . . . . . . . . 12
⊢ (𝐴 = ∅ →
(♯‘𝐴) =
0) |
11 | 10 | oveq1d 7250 |
. . . . . . . . . . 11
⊢ (𝐴 = ∅ →
((♯‘𝐴) + 1) =
(0 + 1)) |
12 | | 0p1e1 11982 |
. . . . . . . . . . 11
⊢ (0 + 1) =
1 |
13 | 11, 12 | eqtrdi 2796 |
. . . . . . . . . 10
⊢ (𝐴 = ∅ →
((♯‘𝐴) + 1) =
1) |
14 | 13 | oveq2d 7251 |
. . . . . . . . 9
⊢ (𝐴 = ∅ →
(1..^((♯‘𝐴) +
1)) = (1..^1)) |
15 | | fzo0 13296 |
. . . . . . . . 9
⊢ (1..^1) =
∅ |
16 | 14, 15 | eqtrdi 2796 |
. . . . . . . 8
⊢ (𝐴 = ∅ →
(1..^((♯‘𝐴) +
1)) = ∅) |
17 | 4, 16 | eqtr4d 2782 |
. . . . . . 7
⊢ (𝐴 = ∅ → dom ∅ =
(1..^((♯‘𝐴) +
1))) |
18 | 17 | olcd 874 |
. . . . . 6
⊢ (𝐴 = ∅ → (dom ∅ =
ℕ ∨ dom ∅ = (1..^((♯‘𝐴) + 1)))) |
19 | 7, 18 | jca 515 |
. . . . 5
⊢ (𝐴 = ∅ → (∅:dom
∅–1-1-onto→𝐴 ∧ (dom ∅ = ℕ ∨ dom
∅ = (1..^((♯‘𝐴) + 1))))) |
20 | | 0ex 5217 |
. . . . . 6
⊢ ∅
∈ V |
21 | | id 22 |
. . . . . . . 8
⊢ (𝑓 = ∅ → 𝑓 = ∅) |
22 | | dmeq 5790 |
. . . . . . . 8
⊢ (𝑓 = ∅ → dom 𝑓 = dom ∅) |
23 | | eqidd 2740 |
. . . . . . . 8
⊢ (𝑓 = ∅ → 𝐴 = 𝐴) |
24 | 21, 22, 23 | f1oeq123d 6677 |
. . . . . . 7
⊢ (𝑓 = ∅ → (𝑓:dom 𝑓–1-1-onto→𝐴 ↔ ∅:dom
∅–1-1-onto→𝐴)) |
25 | 22 | eqeq1d 2741 |
. . . . . . . 8
⊢ (𝑓 = ∅ → (dom 𝑓 = ℕ ↔ dom ∅ =
ℕ)) |
26 | 22 | eqeq1d 2741 |
. . . . . . . 8
⊢ (𝑓 = ∅ → (dom 𝑓 = (1..^((♯‘𝐴) + 1)) ↔ dom ∅ =
(1..^((♯‘𝐴) +
1)))) |
27 | 25, 26 | orbi12d 919 |
. . . . . . 7
⊢ (𝑓 = ∅ → ((dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1))) ↔ (dom ∅ =
ℕ ∨ dom ∅ = (1..^((♯‘𝐴) + 1))))) |
28 | 24, 27 | anbi12d 634 |
. . . . . 6
⊢ (𝑓 = ∅ → ((𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1)))) ↔ (∅:dom
∅–1-1-onto→𝐴 ∧ (dom ∅ = ℕ ∨ dom
∅ = (1..^((♯‘𝐴) + 1)))))) |
29 | 20, 28 | spcev 3536 |
. . . . 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 485 |
. . 3
⊢ (((𝐴 ≼ ω ∧ 𝐴 ∈ Fin) ∧ 𝐴 = ∅) → ∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1))))) |
32 | | f1odm 6687 |
. . . . . . . . . . 11
⊢ (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → dom 𝑓 = (1...(♯‘𝐴))) |
33 | 32 | f1oeq2d 6679 |
. . . . . . . . . 10
⊢ (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → (𝑓:dom 𝑓–1-1-onto→𝐴 ↔ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) |
34 | 33 | ibir 271 |
. . . . . . . . 9
⊢ (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝑓:dom 𝑓–1-1-onto→𝐴) |
35 | 34 | adantl 485 |
. . . . . . . 8
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝑓:dom 𝑓–1-1-onto→𝐴) |
36 | 32 | adantl 485 |
. . . . . . . . . 10
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → dom 𝑓 = (1...(♯‘𝐴))) |
37 | | simpl 486 |
. . . . . . . . . . . 12
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → (♯‘𝐴) ∈
ℕ) |
38 | 37 | nnzd 12311 |
. . . . . . . . . . 11
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → (♯‘𝐴) ∈
ℤ) |
39 | | fzval3 13341 |
. . . . . . . . . . 11
⊢
((♯‘𝐴)
∈ ℤ → (1...(♯‘𝐴)) = (1..^((♯‘𝐴) + 1))) |
40 | 38, 39 | syl 17 |
. . . . . . . . . 10
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) →
(1...(♯‘𝐴)) =
(1..^((♯‘𝐴) +
1))) |
41 | 36, 40 | eqtrd 2779 |
. . . . . . . . 9
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → dom 𝑓 = (1..^((♯‘𝐴) + 1))) |
42 | 41 | olcd 874 |
. . . . . . . 8
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1)))) |
43 | 35, 42 | jca 515 |
. . . . . . 7
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → (𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1))))) |
44 | 43 | ex 416 |
. . . . . 6
⊢
((♯‘𝐴)
∈ ℕ → (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → (𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1)))))) |
45 | 44 | eximdv 1925 |
. . . . 5
⊢
((♯‘𝐴)
∈ ℕ → (∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → ∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1)))))) |
46 | 45 | imp 410 |
. . . 4
⊢
(((♯‘𝐴)
∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → ∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1))))) |
47 | 46 | adantl 485 |
. . 3
⊢ (((𝐴 ≼ ω ∧ 𝐴 ∈ Fin) ∧
((♯‘𝐴) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1))))) |
48 | | fz1f1o 15307 |
. . . 4
⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨
((♯‘𝐴) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))) |
49 | 48 | adantl 485 |
. . 3
⊢ ((𝐴 ≼ ω ∧ 𝐴 ∈ Fin) → (𝐴 = ∅ ∨
((♯‘𝐴) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))) |
50 | 31, 47, 49 | mpjaodan 959 |
. 2
⊢ ((𝐴 ≼ ω ∧ 𝐴 ∈ Fin) → ∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1))))) |
51 | | isfinite 9297 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Fin ↔ 𝐴 ≺
ω) |
52 | 51 | notbii 323 |
. . . . . . . . 9
⊢ (¬
𝐴 ∈ Fin ↔ ¬
𝐴 ≺
ω) |
53 | 52 | biimpi 219 |
. . . . . . . 8
⊢ (¬
𝐴 ∈ Fin → ¬
𝐴 ≺
ω) |
54 | 53 | anim2i 620 |
. . . . . . 7
⊢ ((𝐴 ≼ ω ∧ ¬
𝐴 ∈ Fin) → (𝐴 ≼ ω ∧ ¬
𝐴 ≺
ω)) |
55 | | bren2 8685 |
. . . . . . 7
⊢ (𝐴 ≈ ω ↔ (𝐴 ≼ ω ∧ ¬
𝐴 ≺
ω)) |
56 | 54, 55 | sylibr 237 |
. . . . . 6
⊢ ((𝐴 ≼ ω ∧ ¬
𝐴 ∈ Fin) → 𝐴 ≈
ω) |
57 | | nnenom 13585 |
. . . . . . 7
⊢ ℕ
≈ ω |
58 | 57 | ensymi 8704 |
. . . . . 6
⊢ ω
≈ ℕ |
59 | | entr 8706 |
. . . . . 6
⊢ ((𝐴 ≈ ω ∧ ω
≈ ℕ) → 𝐴
≈ ℕ) |
60 | 56, 58, 59 | sylancl 589 |
. . . . 5
⊢ ((𝐴 ≼ ω ∧ ¬
𝐴 ∈ Fin) → 𝐴 ≈
ℕ) |
61 | | bren 8660 |
. . . . 5
⊢ (𝐴 ≈ ℕ ↔
∃𝑔 𝑔:𝐴–1-1-onto→ℕ) |
62 | 60, 61 | sylib 221 |
. . . 4
⊢ ((𝐴 ≼ ω ∧ ¬
𝐴 ∈ Fin) →
∃𝑔 𝑔:𝐴–1-1-onto→ℕ) |
63 | | f1oexbi 7728 |
. . . 4
⊢
(∃𝑔 𝑔:𝐴–1-1-onto→ℕ ↔ ∃𝑓 𝑓:ℕ–1-1-onto→𝐴) |
64 | 62, 63 | sylib 221 |
. . 3
⊢ ((𝐴 ≼ ω ∧ ¬
𝐴 ∈ Fin) →
∃𝑓 𝑓:ℕ–1-1-onto→𝐴) |
65 | | f1odm 6687 |
. . . . . . 7
⊢ (𝑓:ℕ–1-1-onto→𝐴 → dom 𝑓 = ℕ) |
66 | 65 | f1oeq2d 6679 |
. . . . . 6
⊢ (𝑓:ℕ–1-1-onto→𝐴 → (𝑓:dom 𝑓–1-1-onto→𝐴 ↔ 𝑓:ℕ–1-1-onto→𝐴)) |
67 | 66 | ibir 271 |
. . . . 5
⊢ (𝑓:ℕ–1-1-onto→𝐴 → 𝑓:dom 𝑓–1-1-onto→𝐴) |
68 | 65 | orcd 873 |
. . . . 5
⊢ (𝑓:ℕ–1-1-onto→𝐴 → (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1)))) |
69 | 67, 68 | jca 515 |
. . . 4
⊢ (𝑓:ℕ–1-1-onto→𝐴 → (𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1))))) |
70 | 69 | eximi 1842 |
. . 3
⊢
(∃𝑓 𝑓:ℕ–1-1-onto→𝐴 → ∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1))))) |
71 | 64, 70 | syl 17 |
. 2
⊢ ((𝐴 ≼ ω ∧ ¬
𝐴 ∈ Fin) →
∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1))))) |
72 | 50, 71 | pm2.61dan 813 |
1
⊢ (𝐴 ≼ ω →
∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1))))) |