| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ackbij.f | . . 3
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) | 
| 2 | 1 | ackbij1lem17 10276 | . 2
⊢ 𝐹:(𝒫 ω ∩
Fin)–1-1→ω | 
| 3 |  | f1f 6803 | . . . 4
⊢ (𝐹:(𝒫 ω ∩
Fin)–1-1→ω → 𝐹:(𝒫 ω ∩
Fin)⟶ω) | 
| 4 |  | frn 6742 | . . . 4
⊢ (𝐹:(𝒫 ω ∩
Fin)⟶ω → ran 𝐹 ⊆ ω) | 
| 5 | 2, 3, 4 | mp2b 10 | . . 3
⊢ ran 𝐹 ⊆
ω | 
| 6 |  | eleq1 2828 | . . . . 5
⊢ (𝑏 = ∅ → (𝑏 ∈ ran 𝐹 ↔ ∅ ∈ ran 𝐹)) | 
| 7 |  | eleq1 2828 | . . . . 5
⊢ (𝑏 = 𝑎 → (𝑏 ∈ ran 𝐹 ↔ 𝑎 ∈ ran 𝐹)) | 
| 8 |  | eleq1 2828 | . . . . 5
⊢ (𝑏 = suc 𝑎 → (𝑏 ∈ ran 𝐹 ↔ suc 𝑎 ∈ ran 𝐹)) | 
| 9 |  | peano1 7911 | . . . . . . . 8
⊢ ∅
∈ ω | 
| 10 |  | ackbij1lem3 10262 | . . . . . . . 8
⊢ (∅
∈ ω → ∅ ∈ (𝒫 ω ∩
Fin)) | 
| 11 | 9, 10 | ax-mp 5 | . . . . . . 7
⊢ ∅
∈ (𝒫 ω ∩ Fin) | 
| 12 | 1 | ackbij1lem13 10272 | . . . . . . 7
⊢ (𝐹‘∅) =
∅ | 
| 13 |  | fveqeq2 6914 | . . . . . . . 8
⊢ (𝑎 = ∅ → ((𝐹‘𝑎) = ∅ ↔ (𝐹‘∅) = ∅)) | 
| 14 | 13 | rspcev 3621 | . . . . . . 7
⊢ ((∅
∈ (𝒫 ω ∩ Fin) ∧ (𝐹‘∅) = ∅) →
∃𝑎 ∈ (𝒫
ω ∩ Fin)(𝐹‘𝑎) = ∅) | 
| 15 | 11, 12, 14 | mp2an 692 | . . . . . 6
⊢
∃𝑎 ∈
(𝒫 ω ∩ Fin)(𝐹‘𝑎) = ∅ | 
| 16 |  | f1fn 6804 | . . . . . . . 8
⊢ (𝐹:(𝒫 ω ∩
Fin)–1-1→ω → 𝐹 Fn (𝒫 ω ∩
Fin)) | 
| 17 | 2, 16 | ax-mp 5 | . . . . . . 7
⊢ 𝐹 Fn (𝒫 ω ∩
Fin) | 
| 18 |  | fvelrnb 6968 | . . . . . . 7
⊢ (𝐹 Fn (𝒫 ω ∩
Fin) → (∅ ∈ ran 𝐹 ↔ ∃𝑎 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑎) = ∅)) | 
| 19 | 17, 18 | ax-mp 5 | . . . . . 6
⊢ (∅
∈ ran 𝐹 ↔
∃𝑎 ∈ (𝒫
ω ∩ Fin)(𝐹‘𝑎) = ∅) | 
| 20 | 15, 19 | mpbir 231 | . . . . 5
⊢ ∅
∈ ran 𝐹 | 
| 21 | 1 | ackbij1lem18 10277 | . . . . . . . . 9
⊢ (𝑐 ∈ (𝒫 ω ∩
Fin) → ∃𝑏 ∈
(𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc (𝐹‘𝑐)) | 
| 22 | 21 | adantl 481 | . . . . . . . 8
⊢ ((𝑎 ∈ ω ∧ 𝑐 ∈ (𝒫 ω ∩
Fin)) → ∃𝑏
∈ (𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc (𝐹‘𝑐)) | 
| 23 |  | suceq 6449 | . . . . . . . . . 10
⊢ ((𝐹‘𝑐) = 𝑎 → suc (𝐹‘𝑐) = suc 𝑎) | 
| 24 | 23 | eqeq2d 2747 | . . . . . . . . 9
⊢ ((𝐹‘𝑐) = 𝑎 → ((𝐹‘𝑏) = suc (𝐹‘𝑐) ↔ (𝐹‘𝑏) = suc 𝑎)) | 
| 25 | 24 | rexbidv 3178 | . . . . . . . 8
⊢ ((𝐹‘𝑐) = 𝑎 → (∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc (𝐹‘𝑐) ↔ ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc 𝑎)) | 
| 26 | 22, 25 | syl5ibcom 245 | . . . . . . 7
⊢ ((𝑎 ∈ ω ∧ 𝑐 ∈ (𝒫 ω ∩
Fin)) → ((𝐹‘𝑐) = 𝑎 → ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc 𝑎)) | 
| 27 | 26 | rexlimdva 3154 | . . . . . 6
⊢ (𝑎 ∈ ω →
(∃𝑐 ∈ (𝒫
ω ∩ Fin)(𝐹‘𝑐) = 𝑎 → ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc 𝑎)) | 
| 28 |  | fvelrnb 6968 | . . . . . . 7
⊢ (𝐹 Fn (𝒫 ω ∩
Fin) → (𝑎 ∈ ran
𝐹 ↔ ∃𝑐 ∈ (𝒫 ω ∩
Fin)(𝐹‘𝑐) = 𝑎)) | 
| 29 | 17, 28 | ax-mp 5 | . . . . . 6
⊢ (𝑎 ∈ ran 𝐹 ↔ ∃𝑐 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑐) = 𝑎) | 
| 30 |  | fvelrnb 6968 | . . . . . . 7
⊢ (𝐹 Fn (𝒫 ω ∩
Fin) → (suc 𝑎 ∈
ran 𝐹 ↔ ∃𝑏 ∈ (𝒫 ω ∩
Fin)(𝐹‘𝑏) = suc 𝑎)) | 
| 31 | 17, 30 | ax-mp 5 | . . . . . 6
⊢ (suc
𝑎 ∈ ran 𝐹 ↔ ∃𝑏 ∈ (𝒫 ω ∩
Fin)(𝐹‘𝑏) = suc 𝑎) | 
| 32 | 27, 29, 31 | 3imtr4g 296 | . . . . 5
⊢ (𝑎 ∈ ω → (𝑎 ∈ ran 𝐹 → suc 𝑎 ∈ ran 𝐹)) | 
| 33 | 6, 7, 8, 7, 20, 32 | finds 7919 | . . . 4
⊢ (𝑎 ∈ ω → 𝑎 ∈ ran 𝐹) | 
| 34 | 33 | ssriv 3986 | . . 3
⊢ ω
⊆ ran 𝐹 | 
| 35 | 5, 34 | eqssi 3999 | . 2
⊢ ran 𝐹 = ω | 
| 36 |  | dff1o5 6856 | . 2
⊢ (𝐹:(𝒫 ω ∩
Fin)–1-1-onto→ω ↔ (𝐹:(𝒫 ω ∩ Fin)–1-1→ω ∧ ran 𝐹 = ω)) | 
| 37 | 2, 35, 36 | mpbir2an 711 | 1
⊢ 𝐹:(𝒫 ω ∩
Fin)–1-1-onto→ω |