| Step | Hyp | Ref
| Expression |
| 1 | | f1o0 6885 |
. . . . . . 7
⊢
∅:∅–1-1-onto→∅ |
| 2 | | eqidd 2738 |
. . . . . . . 8
⊢ (𝐴 = ∅ → ∅ =
∅) |
| 3 | | dm0 5931 |
. . . . . . . . 9
⊢ dom
∅ = ∅ |
| 4 | 3 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 = ∅ → dom ∅ =
∅) |
| 5 | | id 22 |
. . . . . . . 8
⊢ (𝐴 = ∅ → 𝐴 = ∅) |
| 6 | 2, 4, 5 | f1oeq123d 6842 |
. . . . . . 7
⊢ (𝐴 = ∅ → (∅:dom
∅–1-1-onto→𝐴 ↔ ∅:∅–1-1-onto→∅)) |
| 7 | 1, 6 | mpbiri 258 |
. . . . . 6
⊢ (𝐴 = ∅ → ∅:dom
∅–1-1-onto→𝐴) |
| 8 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝐴 = ∅ →
(♯‘𝐴) =
(♯‘∅)) |
| 9 | | hash0 14406 |
. . . . . . . . . . . . 13
⊢
(♯‘∅) = 0 |
| 10 | 8, 9 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ (𝐴 = ∅ →
(♯‘𝐴) =
0) |
| 11 | 10 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝐴 = ∅ →
((♯‘𝐴) + 1) =
(0 + 1)) |
| 12 | | 0p1e1 12388 |
. . . . . . . . . . 11
⊢ (0 + 1) =
1 |
| 13 | 11, 12 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝐴 = ∅ →
((♯‘𝐴) + 1) =
1) |
| 14 | 13 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝐴 = ∅ →
(1..^((♯‘𝐴) +
1)) = (1..^1)) |
| 15 | | fzo0 13723 |
. . . . . . . . 9
⊢ (1..^1) =
∅ |
| 16 | 14, 15 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝐴 = ∅ →
(1..^((♯‘𝐴) +
1)) = ∅) |
| 17 | 4, 16 | eqtr4d 2780 |
. . . . . . 7
⊢ (𝐴 = ∅ → dom ∅ =
(1..^((♯‘𝐴) +
1))) |
| 18 | 17 | olcd 875 |
. . . . . 6
⊢ (𝐴 = ∅ → (dom ∅ =
ℕ ∨ dom ∅ = (1..^((♯‘𝐴) + 1)))) |
| 19 | 7, 18 | jca 511 |
. . . . 5
⊢ (𝐴 = ∅ → (∅:dom
∅–1-1-onto→𝐴 ∧ (dom ∅ = ℕ ∨ dom
∅ = (1..^((♯‘𝐴) + 1))))) |
| 20 | | 0ex 5307 |
. . . . . 6
⊢ ∅
∈ V |
| 21 | | id 22 |
. . . . . . . 8
⊢ (𝑓 = ∅ → 𝑓 = ∅) |
| 22 | | dmeq 5914 |
. . . . . . . 8
⊢ (𝑓 = ∅ → dom 𝑓 = dom ∅) |
| 23 | | eqidd 2738 |
. . . . . . . 8
⊢ (𝑓 = ∅ → 𝐴 = 𝐴) |
| 24 | 21, 22, 23 | f1oeq123d 6842 |
. . . . . . 7
⊢ (𝑓 = ∅ → (𝑓:dom 𝑓–1-1-onto→𝐴 ↔ ∅:dom
∅–1-1-onto→𝐴)) |
| 25 | 22 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑓 = ∅ → (dom 𝑓 = ℕ ↔ dom ∅ =
ℕ)) |
| 26 | 22 | eqeq1d 2739 |
. . . . . . . 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 632 |
. . . . . 6
⊢ (𝑓 = ∅ → ((𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1)))) ↔ (∅:dom
∅–1-1-onto→𝐴 ∧ (dom ∅ = ℕ ∨ dom
∅ = (1..^((♯‘𝐴) + 1)))))) |
| 29 | 20, 28 | spcev 3606 |
. . . . 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 481 |
. . 3
⊢ (((𝐴 ≼ ω ∧ 𝐴 ∈ Fin) ∧ 𝐴 = ∅) → ∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1))))) |
| 32 | | f1odm 6852 |
. . . . . . . . . . 11
⊢ (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → dom 𝑓 = (1...(♯‘𝐴))) |
| 33 | 32 | f1oeq2d 6844 |
. . . . . . . . . 10
⊢ (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → (𝑓:dom 𝑓–1-1-onto→𝐴 ↔ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) |
| 34 | 33 | ibir 268 |
. . . . . . . . 9
⊢ (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝑓:dom 𝑓–1-1-onto→𝐴) |
| 35 | 34 | adantl 481 |
. . . . . . . 8
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝑓:dom 𝑓–1-1-onto→𝐴) |
| 36 | 32 | adantl 481 |
. . . . . . . . . 10
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → dom 𝑓 = (1...(♯‘𝐴))) |
| 37 | | simpl 482 |
. . . . . . . . . . . 12
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → (♯‘𝐴) ∈
ℕ) |
| 38 | 37 | nnzd 12640 |
. . . . . . . . . . 11
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → (♯‘𝐴) ∈
ℤ) |
| 39 | | fzval3 13773 |
. . . . . . . . . . 11
⊢
((♯‘𝐴)
∈ ℤ → (1...(♯‘𝐴)) = (1..^((♯‘𝐴) + 1))) |
| 40 | 38, 39 | syl 17 |
. . . . . . . . . 10
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) →
(1...(♯‘𝐴)) =
(1..^((♯‘𝐴) +
1))) |
| 41 | 36, 40 | eqtrd 2777 |
. . . . . . . . 9
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → dom 𝑓 = (1..^((♯‘𝐴) + 1))) |
| 42 | 41 | olcd 875 |
. . . . . . . 8
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1)))) |
| 43 | 35, 42 | jca 511 |
. . . . . . 7
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → (𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1))))) |
| 44 | 43 | ex 412 |
. . . . . 6
⊢
((♯‘𝐴)
∈ ℕ → (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → (𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1)))))) |
| 45 | 44 | eximdv 1917 |
. . . . 5
⊢
((♯‘𝐴)
∈ ℕ → (∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → ∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1)))))) |
| 46 | 45 | imp 406 |
. . . 4
⊢
(((♯‘𝐴)
∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → ∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1))))) |
| 47 | 46 | adantl 481 |
. . 3
⊢ (((𝐴 ≼ ω ∧ 𝐴 ∈ Fin) ∧
((♯‘𝐴) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1))))) |
| 48 | | fz1f1o 15746 |
. . . 4
⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨
((♯‘𝐴) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))) |
| 49 | 48 | adantl 481 |
. . 3
⊢ ((𝐴 ≼ ω ∧ 𝐴 ∈ Fin) → (𝐴 = ∅ ∨
((♯‘𝐴) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))) |
| 50 | 31, 47, 49 | mpjaodan 961 |
. 2
⊢ ((𝐴 ≼ ω ∧ 𝐴 ∈ Fin) → ∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1))))) |
| 51 | | isfinite 9692 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Fin ↔ 𝐴 ≺
ω) |
| 52 | 51 | notbii 320 |
. . . . . . . . 9
⊢ (¬
𝐴 ∈ Fin ↔ ¬
𝐴 ≺
ω) |
| 53 | 52 | biimpi 216 |
. . . . . . . 8
⊢ (¬
𝐴 ∈ Fin → ¬
𝐴 ≺
ω) |
| 54 | 53 | anim2i 617 |
. . . . . . 7
⊢ ((𝐴 ≼ ω ∧ ¬
𝐴 ∈ Fin) → (𝐴 ≼ ω ∧ ¬
𝐴 ≺
ω)) |
| 55 | | bren2 9023 |
. . . . . . 7
⊢ (𝐴 ≈ ω ↔ (𝐴 ≼ ω ∧ ¬
𝐴 ≺
ω)) |
| 56 | 54, 55 | sylibr 234 |
. . . . . 6
⊢ ((𝐴 ≼ ω ∧ ¬
𝐴 ∈ Fin) → 𝐴 ≈
ω) |
| 57 | | nnenom 14021 |
. . . . . . 7
⊢ ℕ
≈ ω |
| 58 | 57 | ensymi 9044 |
. . . . . 6
⊢ ω
≈ ℕ |
| 59 | | entr 9046 |
. . . . . 6
⊢ ((𝐴 ≈ ω ∧ ω
≈ ℕ) → 𝐴
≈ ℕ) |
| 60 | 56, 58, 59 | sylancl 586 |
. . . . 5
⊢ ((𝐴 ≼ ω ∧ ¬
𝐴 ∈ Fin) → 𝐴 ≈
ℕ) |
| 61 | | bren 8995 |
. . . . 5
⊢ (𝐴 ≈ ℕ ↔
∃𝑔 𝑔:𝐴–1-1-onto→ℕ) |
| 62 | 60, 61 | sylib 218 |
. . . 4
⊢ ((𝐴 ≼ ω ∧ ¬
𝐴 ∈ Fin) →
∃𝑔 𝑔:𝐴–1-1-onto→ℕ) |
| 63 | | f1oexbi 7950 |
. . . 4
⊢
(∃𝑔 𝑔:𝐴–1-1-onto→ℕ ↔ ∃𝑓 𝑓:ℕ–1-1-onto→𝐴) |
| 64 | 62, 63 | sylib 218 |
. . 3
⊢ ((𝐴 ≼ ω ∧ ¬
𝐴 ∈ Fin) →
∃𝑓 𝑓:ℕ–1-1-onto→𝐴) |
| 65 | | f1odm 6852 |
. . . . . . 7
⊢ (𝑓:ℕ–1-1-onto→𝐴 → dom 𝑓 = ℕ) |
| 66 | 65 | f1oeq2d 6844 |
. . . . . 6
⊢ (𝑓:ℕ–1-1-onto→𝐴 → (𝑓:dom 𝑓–1-1-onto→𝐴 ↔ 𝑓:ℕ–1-1-onto→𝐴)) |
| 67 | 66 | ibir 268 |
. . . . 5
⊢ (𝑓:ℕ–1-1-onto→𝐴 → 𝑓:dom 𝑓–1-1-onto→𝐴) |
| 68 | 65 | orcd 874 |
. . . . 5
⊢ (𝑓:ℕ–1-1-onto→𝐴 → (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1)))) |
| 69 | 67, 68 | jca 511 |
. . . 4
⊢ (𝑓:ℕ–1-1-onto→𝐴 → (𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1))))) |
| 70 | 69 | eximi 1835 |
. . 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))))) |