Step | Hyp | Ref
| Expression |
1 | | ackbij.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) |
2 | 1 | ackbij1lem17 8941 |
. 2
⊢ 𝐹:(𝒫 ω ∩
Fin)–1-1→ω |
3 | | f1f 6014 |
. . . 4
⊢ (𝐹:(𝒫 ω ∩
Fin)–1-1→ω → 𝐹:(𝒫 ω ∩
Fin)⟶ω) |
4 | | frn 5966 |
. . . 4
⊢ (𝐹:(𝒫 ω ∩
Fin)⟶ω → ran 𝐹 ⊆ ω) |
5 | 2, 3, 4 | mp2b 10 |
. . 3
⊢ ran 𝐹 ⊆
ω |
6 | | eleq1 2676 |
. . . . 5
⊢ (𝑏 = ∅ → (𝑏 ∈ ran 𝐹 ↔ ∅ ∈ ran 𝐹)) |
7 | | eleq1 2676 |
. . . . 5
⊢ (𝑏 = 𝑎 → (𝑏 ∈ ran 𝐹 ↔ 𝑎 ∈ ran 𝐹)) |
8 | | eleq1 2676 |
. . . . 5
⊢ (𝑏 = suc 𝑎 → (𝑏 ∈ ran 𝐹 ↔ suc 𝑎 ∈ ran 𝐹)) |
9 | | peano1 6977 |
. . . . . . . 8
⊢ ∅
∈ ω |
10 | | ackbij1lem3 8927 |
. . . . . . . 8
⊢ (∅
∈ ω → ∅ ∈ (𝒫 ω ∩
Fin)) |
11 | 9, 10 | ax-mp 5 |
. . . . . . 7
⊢ ∅
∈ (𝒫 ω ∩ Fin) |
12 | 1 | ackbij1lem13 8937 |
. . . . . . 7
⊢ (𝐹‘∅) =
∅ |
13 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑎 = ∅ → (𝐹‘𝑎) = (𝐹‘∅)) |
14 | 13 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑎 = ∅ → ((𝐹‘𝑎) = ∅ ↔ (𝐹‘∅) = ∅)) |
15 | 14 | rspcev 3282 |
. . . . . . 7
⊢ ((∅
∈ (𝒫 ω ∩ Fin) ∧ (𝐹‘∅) = ∅) →
∃𝑎 ∈ (𝒫
ω ∩ Fin)(𝐹‘𝑎) = ∅) |
16 | 11, 12, 15 | mp2an 704 |
. . . . . 6
⊢
∃𝑎 ∈
(𝒫 ω ∩ Fin)(𝐹‘𝑎) = ∅ |
17 | | f1fn 6015 |
. . . . . . . 8
⊢ (𝐹:(𝒫 ω ∩
Fin)–1-1→ω → 𝐹 Fn (𝒫 ω ∩
Fin)) |
18 | 2, 17 | ax-mp 5 |
. . . . . . 7
⊢ 𝐹 Fn (𝒫 ω ∩
Fin) |
19 | | fvelrnb 6153 |
. . . . . . 7
⊢ (𝐹 Fn (𝒫 ω ∩
Fin) → (∅ ∈ ran 𝐹 ↔ ∃𝑎 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑎) = ∅)) |
20 | 18, 19 | ax-mp 5 |
. . . . . 6
⊢ (∅
∈ ran 𝐹 ↔
∃𝑎 ∈ (𝒫
ω ∩ Fin)(𝐹‘𝑎) = ∅) |
21 | 16, 20 | mpbir 220 |
. . . . 5
⊢ ∅
∈ ran 𝐹 |
22 | 1 | ackbij1lem18 8942 |
. . . . . . . . 9
⊢ (𝑐 ∈ (𝒫 ω ∩
Fin) → ∃𝑏 ∈
(𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc (𝐹‘𝑐)) |
23 | 22 | adantl 481 |
. . . . . . . 8
⊢ ((𝑎 ∈ ω ∧ 𝑐 ∈ (𝒫 ω ∩
Fin)) → ∃𝑏
∈ (𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc (𝐹‘𝑐)) |
24 | | suceq 5707 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑐) = 𝑎 → suc (𝐹‘𝑐) = suc 𝑎) |
25 | 24 | eqeq2d 2620 |
. . . . . . . . 9
⊢ ((𝐹‘𝑐) = 𝑎 → ((𝐹‘𝑏) = suc (𝐹‘𝑐) ↔ (𝐹‘𝑏) = suc 𝑎)) |
26 | 25 | rexbidv 3034 |
. . . . . . . 8
⊢ ((𝐹‘𝑐) = 𝑎 → (∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc (𝐹‘𝑐) ↔ ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc 𝑎)) |
27 | 23, 26 | syl5ibcom 234 |
. . . . . . 7
⊢ ((𝑎 ∈ ω ∧ 𝑐 ∈ (𝒫 ω ∩
Fin)) → ((𝐹‘𝑐) = 𝑎 → ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc 𝑎)) |
28 | 27 | rexlimdva 3013 |
. . . . . 6
⊢ (𝑎 ∈ ω →
(∃𝑐 ∈ (𝒫
ω ∩ Fin)(𝐹‘𝑐) = 𝑎 → ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc 𝑎)) |
29 | | fvelrnb 6153 |
. . . . . . 7
⊢ (𝐹 Fn (𝒫 ω ∩
Fin) → (𝑎 ∈ ran
𝐹 ↔ ∃𝑐 ∈ (𝒫 ω ∩
Fin)(𝐹‘𝑐) = 𝑎)) |
30 | 18, 29 | ax-mp 5 |
. . . . . 6
⊢ (𝑎 ∈ ran 𝐹 ↔ ∃𝑐 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑐) = 𝑎) |
31 | | fvelrnb 6153 |
. . . . . . 7
⊢ (𝐹 Fn (𝒫 ω ∩
Fin) → (suc 𝑎 ∈
ran 𝐹 ↔ ∃𝑏 ∈ (𝒫 ω ∩
Fin)(𝐹‘𝑏) = suc 𝑎)) |
32 | 18, 31 | ax-mp 5 |
. . . . . 6
⊢ (suc
𝑎 ∈ ran 𝐹 ↔ ∃𝑏 ∈ (𝒫 ω ∩
Fin)(𝐹‘𝑏) = suc 𝑎) |
33 | 28, 30, 32 | 3imtr4g 284 |
. . . . 5
⊢ (𝑎 ∈ ω → (𝑎 ∈ ran 𝐹 → suc 𝑎 ∈ ran 𝐹)) |
34 | 6, 7, 8, 7, 21, 33 | finds 6984 |
. . . 4
⊢ (𝑎 ∈ ω → 𝑎 ∈ ran 𝐹) |
35 | 34 | ssriv 3572 |
. . 3
⊢ ω
⊆ ran 𝐹 |
36 | 5, 35 | eqssi 3584 |
. 2
⊢ ran 𝐹 = ω |
37 | | dff1o5 6059 |
. 2
⊢ (𝐹:(𝒫 ω ∩
Fin)–1-1-onto→ω ↔ (𝐹:(𝒫 ω ∩ Fin)–1-1→ω ∧ ran 𝐹 = ω)) |
38 | 2, 36, 37 | mpbir2an 957 |
1
⊢ 𝐹:(𝒫 ω ∩
Fin)–1-1-onto→ω |