Step |
Hyp |
Ref |
Expression |
1 |
|
ackbij.f |
⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) ) |
2 |
1
|
ackbij1lem10 |
⊢ 𝐹 : ( 𝒫 ω ∩ Fin ) ⟶ ω |
3 |
|
peano1 |
⊢ ∅ ∈ ω |
4 |
2 3
|
f0cli |
⊢ ( 𝐹 ‘ ∅ ) ∈ ω |
5 |
|
nna0 |
⊢ ( ( 𝐹 ‘ ∅ ) ∈ ω → ( ( 𝐹 ‘ ∅ ) +o ∅ ) = ( 𝐹 ‘ ∅ ) ) |
6 |
4 5
|
ax-mp |
⊢ ( ( 𝐹 ‘ ∅ ) +o ∅ ) = ( 𝐹 ‘ ∅ ) |
7 |
|
un0 |
⊢ ( ∅ ∪ ∅ ) = ∅ |
8 |
7
|
fveq2i |
⊢ ( 𝐹 ‘ ( ∅ ∪ ∅ ) ) = ( 𝐹 ‘ ∅ ) |
9 |
|
ackbij1lem3 |
⊢ ( ∅ ∈ ω → ∅ ∈ ( 𝒫 ω ∩ Fin ) ) |
10 |
3 9
|
ax-mp |
⊢ ∅ ∈ ( 𝒫 ω ∩ Fin ) |
11 |
|
in0 |
⊢ ( ∅ ∩ ∅ ) = ∅ |
12 |
1
|
ackbij1lem9 |
⊢ ( ( ∅ ∈ ( 𝒫 ω ∩ Fin ) ∧ ∅ ∈ ( 𝒫 ω ∩ Fin ) ∧ ( ∅ ∩ ∅ ) = ∅ ) → ( 𝐹 ‘ ( ∅ ∪ ∅ ) ) = ( ( 𝐹 ‘ ∅ ) +o ( 𝐹 ‘ ∅ ) ) ) |
13 |
10 10 11 12
|
mp3an |
⊢ ( 𝐹 ‘ ( ∅ ∪ ∅ ) ) = ( ( 𝐹 ‘ ∅ ) +o ( 𝐹 ‘ ∅ ) ) |
14 |
6 8 13
|
3eqtr2ri |
⊢ ( ( 𝐹 ‘ ∅ ) +o ( 𝐹 ‘ ∅ ) ) = ( ( 𝐹 ‘ ∅ ) +o ∅ ) |
15 |
|
nnacan |
⊢ ( ( ( 𝐹 ‘ ∅ ) ∈ ω ∧ ( 𝐹 ‘ ∅ ) ∈ ω ∧ ∅ ∈ ω ) → ( ( ( 𝐹 ‘ ∅ ) +o ( 𝐹 ‘ ∅ ) ) = ( ( 𝐹 ‘ ∅ ) +o ∅ ) ↔ ( 𝐹 ‘ ∅ ) = ∅ ) ) |
16 |
4 4 3 15
|
mp3an |
⊢ ( ( ( 𝐹 ‘ ∅ ) +o ( 𝐹 ‘ ∅ ) ) = ( ( 𝐹 ‘ ∅ ) +o ∅ ) ↔ ( 𝐹 ‘ ∅ ) = ∅ ) |
17 |
14 16
|
mpbi |
⊢ ( 𝐹 ‘ ∅ ) = ∅ |