| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ackbij.f | . . 3
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) | 
| 2 | 1 | ackbij1lem8 10267 | . 2
⊢ (𝐴 ∈ ω → (𝐹‘{𝐴}) = (card‘𝒫 𝐴)) | 
| 3 |  | pweq 4613 | . . . . 5
⊢ (𝑎 = ∅ → 𝒫
𝑎 = 𝒫
∅) | 
| 4 | 3 | fveq2d 6909 | . . . 4
⊢ (𝑎 = ∅ →
(card‘𝒫 𝑎) =
(card‘𝒫 ∅)) | 
| 5 |  | fveq2 6905 | . . . . 5
⊢ (𝑎 = ∅ → (𝐹‘𝑎) = (𝐹‘∅)) | 
| 6 |  | suceq 6449 | . . . . 5
⊢ ((𝐹‘𝑎) = (𝐹‘∅) → suc (𝐹‘𝑎) = suc (𝐹‘∅)) | 
| 7 | 5, 6 | syl 17 | . . . 4
⊢ (𝑎 = ∅ → suc (𝐹‘𝑎) = suc (𝐹‘∅)) | 
| 8 | 4, 7 | eqeq12d 2752 | . . 3
⊢ (𝑎 = ∅ →
((card‘𝒫 𝑎) =
suc (𝐹‘𝑎) ↔ (card‘𝒫
∅) = suc (𝐹‘∅))) | 
| 9 |  | pweq 4613 | . . . . 5
⊢ (𝑎 = 𝑏 → 𝒫 𝑎 = 𝒫 𝑏) | 
| 10 | 9 | fveq2d 6909 | . . . 4
⊢ (𝑎 = 𝑏 → (card‘𝒫 𝑎) = (card‘𝒫 𝑏)) | 
| 11 |  | fveq2 6905 | . . . . 5
⊢ (𝑎 = 𝑏 → (𝐹‘𝑎) = (𝐹‘𝑏)) | 
| 12 |  | suceq 6449 | . . . . 5
⊢ ((𝐹‘𝑎) = (𝐹‘𝑏) → suc (𝐹‘𝑎) = suc (𝐹‘𝑏)) | 
| 13 | 11, 12 | syl 17 | . . . 4
⊢ (𝑎 = 𝑏 → suc (𝐹‘𝑎) = suc (𝐹‘𝑏)) | 
| 14 | 10, 13 | eqeq12d 2752 | . . 3
⊢ (𝑎 = 𝑏 → ((card‘𝒫 𝑎) = suc (𝐹‘𝑎) ↔ (card‘𝒫 𝑏) = suc (𝐹‘𝑏))) | 
| 15 |  | pweq 4613 | . . . . 5
⊢ (𝑎 = suc 𝑏 → 𝒫 𝑎 = 𝒫 suc 𝑏) | 
| 16 | 15 | fveq2d 6909 | . . . 4
⊢ (𝑎 = suc 𝑏 → (card‘𝒫 𝑎) = (card‘𝒫 suc
𝑏)) | 
| 17 |  | fveq2 6905 | . . . . 5
⊢ (𝑎 = suc 𝑏 → (𝐹‘𝑎) = (𝐹‘suc 𝑏)) | 
| 18 |  | suceq 6449 | . . . . 5
⊢ ((𝐹‘𝑎) = (𝐹‘suc 𝑏) → suc (𝐹‘𝑎) = suc (𝐹‘suc 𝑏)) | 
| 19 | 17, 18 | syl 17 | . . . 4
⊢ (𝑎 = suc 𝑏 → suc (𝐹‘𝑎) = suc (𝐹‘suc 𝑏)) | 
| 20 | 16, 19 | eqeq12d 2752 | . . 3
⊢ (𝑎 = suc 𝑏 → ((card‘𝒫 𝑎) = suc (𝐹‘𝑎) ↔ (card‘𝒫 suc 𝑏) = suc (𝐹‘suc 𝑏))) | 
| 21 |  | pweq 4613 | . . . . 5
⊢ (𝑎 = 𝐴 → 𝒫 𝑎 = 𝒫 𝐴) | 
| 22 | 21 | fveq2d 6909 | . . . 4
⊢ (𝑎 = 𝐴 → (card‘𝒫 𝑎) = (card‘𝒫 𝐴)) | 
| 23 |  | fveq2 6905 | . . . . 5
⊢ (𝑎 = 𝐴 → (𝐹‘𝑎) = (𝐹‘𝐴)) | 
| 24 |  | suceq 6449 | . . . . 5
⊢ ((𝐹‘𝑎) = (𝐹‘𝐴) → suc (𝐹‘𝑎) = suc (𝐹‘𝐴)) | 
| 25 | 23, 24 | syl 17 | . . . 4
⊢ (𝑎 = 𝐴 → suc (𝐹‘𝑎) = suc (𝐹‘𝐴)) | 
| 26 | 22, 25 | eqeq12d 2752 | . . 3
⊢ (𝑎 = 𝐴 → ((card‘𝒫 𝑎) = suc (𝐹‘𝑎) ↔ (card‘𝒫 𝐴) = suc (𝐹‘𝐴))) | 
| 27 |  | df-1o 8507 | . . . 4
⊢
1o = suc ∅ | 
| 28 |  | pw0 4811 | . . . . . 6
⊢ 𝒫
∅ = {∅} | 
| 29 | 28 | fveq2i 6908 | . . . . 5
⊢
(card‘𝒫 ∅) = (card‘{∅}) | 
| 30 |  | 0ex 5306 | . . . . . 6
⊢ ∅
∈ V | 
| 31 |  | cardsn 10010 | . . . . . 6
⊢ (∅
∈ V → (card‘{∅}) = 1o) | 
| 32 | 30, 31 | ax-mp 5 | . . . . 5
⊢
(card‘{∅}) = 1o | 
| 33 | 29, 32 | eqtri 2764 | . . . 4
⊢
(card‘𝒫 ∅) = 1o | 
| 34 | 1 | ackbij1lem13 10272 | . . . . 5
⊢ (𝐹‘∅) =
∅ | 
| 35 |  | suceq 6449 | . . . . 5
⊢ ((𝐹‘∅) = ∅ →
suc (𝐹‘∅) = suc
∅) | 
| 36 | 34, 35 | ax-mp 5 | . . . 4
⊢ suc
(𝐹‘∅) = suc
∅ | 
| 37 | 27, 33, 36 | 3eqtr4i 2774 | . . 3
⊢
(card‘𝒫 ∅) = suc (𝐹‘∅) | 
| 38 |  | oveq2 7440 | . . . . . 6
⊢
((card‘𝒫 𝑏) = suc (𝐹‘𝑏) → ((card‘𝒫 𝑏) +o
(card‘𝒫 𝑏)) =
((card‘𝒫 𝑏)
+o suc (𝐹‘𝑏))) | 
| 39 | 38 | adantl 481 | . . . . 5
⊢ ((𝑏 ∈ ω ∧
(card‘𝒫 𝑏) =
suc (𝐹‘𝑏)) → ((card‘𝒫
𝑏) +o
(card‘𝒫 𝑏)) =
((card‘𝒫 𝑏)
+o suc (𝐹‘𝑏))) | 
| 40 |  | ackbij1lem5 10264 | . . . . . 6
⊢ (𝑏 ∈ ω →
(card‘𝒫 suc 𝑏) = ((card‘𝒫 𝑏) +o (card‘𝒫 𝑏))) | 
| 41 | 40 | adantr 480 | . . . . 5
⊢ ((𝑏 ∈ ω ∧
(card‘𝒫 𝑏) =
suc (𝐹‘𝑏)) → (card‘𝒫
suc 𝑏) =
((card‘𝒫 𝑏)
+o (card‘𝒫 𝑏))) | 
| 42 |  | df-suc 6389 | . . . . . . . . . 10
⊢ suc 𝑏 = (𝑏 ∪ {𝑏}) | 
| 43 | 42 | equncomi 4159 | . . . . . . . . 9
⊢ suc 𝑏 = ({𝑏} ∪ 𝑏) | 
| 44 | 43 | fveq2i 6908 | . . . . . . . 8
⊢ (𝐹‘suc 𝑏) = (𝐹‘({𝑏} ∪ 𝑏)) | 
| 45 |  | ackbij1lem4 10263 | . . . . . . . . . . 11
⊢ (𝑏 ∈ ω → {𝑏} ∈ (𝒫 ω
∩ Fin)) | 
| 46 | 45 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑏 ∈ ω ∧
(card‘𝒫 𝑏) =
suc (𝐹‘𝑏)) → {𝑏} ∈ (𝒫 ω ∩
Fin)) | 
| 47 |  | ackbij1lem3 10262 | . . . . . . . . . . 11
⊢ (𝑏 ∈ ω → 𝑏 ∈ (𝒫 ω ∩
Fin)) | 
| 48 | 47 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑏 ∈ ω ∧
(card‘𝒫 𝑏) =
suc (𝐹‘𝑏)) → 𝑏 ∈ (𝒫 ω ∩
Fin)) | 
| 49 |  | incom 4208 | . . . . . . . . . . . 12
⊢ ({𝑏} ∩ 𝑏) = (𝑏 ∩ {𝑏}) | 
| 50 |  | nnord 7896 | . . . . . . . . . . . . 13
⊢ (𝑏 ∈ ω → Ord 𝑏) | 
| 51 |  | orddisj 6421 | . . . . . . . . . . . . 13
⊢ (Ord
𝑏 → (𝑏 ∩ {𝑏}) = ∅) | 
| 52 | 50, 51 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑏 ∈ ω → (𝑏 ∩ {𝑏}) = ∅) | 
| 53 | 49, 52 | eqtrid 2788 | . . . . . . . . . . 11
⊢ (𝑏 ∈ ω → ({𝑏} ∩ 𝑏) = ∅) | 
| 54 | 53 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑏 ∈ ω ∧
(card‘𝒫 𝑏) =
suc (𝐹‘𝑏)) → ({𝑏} ∩ 𝑏) = ∅) | 
| 55 | 1 | ackbij1lem9 10268 | . . . . . . . . . 10
⊢ (({𝑏} ∈ (𝒫 ω
∩ Fin) ∧ 𝑏 ∈
(𝒫 ω ∩ Fin) ∧ ({𝑏} ∩ 𝑏) = ∅) → (𝐹‘({𝑏} ∪ 𝑏)) = ((𝐹‘{𝑏}) +o (𝐹‘𝑏))) | 
| 56 | 46, 48, 54, 55 | syl3anc 1372 | . . . . . . . . 9
⊢ ((𝑏 ∈ ω ∧
(card‘𝒫 𝑏) =
suc (𝐹‘𝑏)) → (𝐹‘({𝑏} ∪ 𝑏)) = ((𝐹‘{𝑏}) +o (𝐹‘𝑏))) | 
| 57 | 1 | ackbij1lem8 10267 | . . . . . . . . . . 11
⊢ (𝑏 ∈ ω → (𝐹‘{𝑏}) = (card‘𝒫 𝑏)) | 
| 58 | 57 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑏 ∈ ω ∧
(card‘𝒫 𝑏) =
suc (𝐹‘𝑏)) → (𝐹‘{𝑏}) = (card‘𝒫 𝑏)) | 
| 59 | 58 | oveq1d 7447 | . . . . . . . . 9
⊢ ((𝑏 ∈ ω ∧
(card‘𝒫 𝑏) =
suc (𝐹‘𝑏)) → ((𝐹‘{𝑏}) +o (𝐹‘𝑏)) = ((card‘𝒫 𝑏) +o (𝐹‘𝑏))) | 
| 60 | 56, 59 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝑏 ∈ ω ∧
(card‘𝒫 𝑏) =
suc (𝐹‘𝑏)) → (𝐹‘({𝑏} ∪ 𝑏)) = ((card‘𝒫 𝑏) +o (𝐹‘𝑏))) | 
| 61 | 44, 60 | eqtrid 2788 | . . . . . . 7
⊢ ((𝑏 ∈ ω ∧
(card‘𝒫 𝑏) =
suc (𝐹‘𝑏)) → (𝐹‘suc 𝑏) = ((card‘𝒫 𝑏) +o (𝐹‘𝑏))) | 
| 62 |  | suceq 6449 | . . . . . . 7
⊢ ((𝐹‘suc 𝑏) = ((card‘𝒫 𝑏) +o (𝐹‘𝑏)) → suc (𝐹‘suc 𝑏) = suc ((card‘𝒫 𝑏) +o (𝐹‘𝑏))) | 
| 63 | 61, 62 | syl 17 | . . . . . 6
⊢ ((𝑏 ∈ ω ∧
(card‘𝒫 𝑏) =
suc (𝐹‘𝑏)) → suc (𝐹‘suc 𝑏) = suc ((card‘𝒫 𝑏) +o (𝐹‘𝑏))) | 
| 64 |  | nnfi 9208 | . . . . . . . . . 10
⊢ (𝑏 ∈ ω → 𝑏 ∈ Fin) | 
| 65 |  | pwfi 9358 | . . . . . . . . . 10
⊢ (𝑏 ∈ Fin ↔ 𝒫
𝑏 ∈
Fin) | 
| 66 | 64, 65 | sylib 218 | . . . . . . . . 9
⊢ (𝑏 ∈ ω → 𝒫
𝑏 ∈
Fin) | 
| 67 | 66 | adantr 480 | . . . . . . . 8
⊢ ((𝑏 ∈ ω ∧
(card‘𝒫 𝑏) =
suc (𝐹‘𝑏)) → 𝒫 𝑏 ∈ Fin) | 
| 68 |  | ficardom 10002 | . . . . . . . 8
⊢
(𝒫 𝑏 ∈
Fin → (card‘𝒫 𝑏) ∈ ω) | 
| 69 | 67, 68 | syl 17 | . . . . . . 7
⊢ ((𝑏 ∈ ω ∧
(card‘𝒫 𝑏) =
suc (𝐹‘𝑏)) → (card‘𝒫
𝑏) ∈
ω) | 
| 70 | 1 | ackbij1lem10 10269 | . . . . . . . . 9
⊢ 𝐹:(𝒫 ω ∩
Fin)⟶ω | 
| 71 | 70 | ffvelcdmi 7102 | . . . . . . . 8
⊢ (𝑏 ∈ (𝒫 ω ∩
Fin) → (𝐹‘𝑏) ∈
ω) | 
| 72 | 48, 71 | syl 17 | . . . . . . 7
⊢ ((𝑏 ∈ ω ∧
(card‘𝒫 𝑏) =
suc (𝐹‘𝑏)) → (𝐹‘𝑏) ∈ ω) | 
| 73 |  | nnasuc 8645 | . . . . . . 7
⊢
(((card‘𝒫 𝑏) ∈ ω ∧ (𝐹‘𝑏) ∈ ω) →
((card‘𝒫 𝑏)
+o suc (𝐹‘𝑏)) = suc ((card‘𝒫 𝑏) +o (𝐹‘𝑏))) | 
| 74 | 69, 72, 73 | syl2anc 584 | . . . . . 6
⊢ ((𝑏 ∈ ω ∧
(card‘𝒫 𝑏) =
suc (𝐹‘𝑏)) → ((card‘𝒫
𝑏) +o suc (𝐹‘𝑏)) = suc ((card‘𝒫 𝑏) +o (𝐹‘𝑏))) | 
| 75 | 63, 74 | eqtr4d 2779 | . . . . 5
⊢ ((𝑏 ∈ ω ∧
(card‘𝒫 𝑏) =
suc (𝐹‘𝑏)) → suc (𝐹‘suc 𝑏) = ((card‘𝒫 𝑏) +o suc (𝐹‘𝑏))) | 
| 76 | 39, 41, 75 | 3eqtr4d 2786 | . . . 4
⊢ ((𝑏 ∈ ω ∧
(card‘𝒫 𝑏) =
suc (𝐹‘𝑏)) → (card‘𝒫
suc 𝑏) = suc (𝐹‘suc 𝑏)) | 
| 77 | 76 | ex 412 | . . 3
⊢ (𝑏 ∈ ω →
((card‘𝒫 𝑏) =
suc (𝐹‘𝑏) → (card‘𝒫
suc 𝑏) = suc (𝐹‘suc 𝑏))) | 
| 78 | 8, 14, 20, 26, 37, 77 | finds 7919 | . 2
⊢ (𝐴 ∈ ω →
(card‘𝒫 𝐴) =
suc (𝐹‘𝐴)) | 
| 79 | 2, 78 | eqtrd 2776 | 1
⊢ (𝐴 ∈ ω → (𝐹‘{𝐴}) = suc (𝐹‘𝐴)) |