| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ackbij.f |
|- F = ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ y e. x ( { y } X. ~P y ) ) ) |
| 2 |
1
|
ackbij1lem10 |
|- F : ( ~P _om i^i Fin ) --> _om |
| 3 |
|
peano1 |
|- (/) e. _om |
| 4 |
2 3
|
f0cli |
|- ( F ` (/) ) e. _om |
| 5 |
|
nna0 |
|- ( ( F ` (/) ) e. _om -> ( ( F ` (/) ) +o (/) ) = ( F ` (/) ) ) |
| 6 |
4 5
|
ax-mp |
|- ( ( F ` (/) ) +o (/) ) = ( F ` (/) ) |
| 7 |
|
un0 |
|- ( (/) u. (/) ) = (/) |
| 8 |
7
|
fveq2i |
|- ( F ` ( (/) u. (/) ) ) = ( F ` (/) ) |
| 9 |
|
ackbij1lem3 |
|- ( (/) e. _om -> (/) e. ( ~P _om i^i Fin ) ) |
| 10 |
3 9
|
ax-mp |
|- (/) e. ( ~P _om i^i Fin ) |
| 11 |
|
in0 |
|- ( (/) i^i (/) ) = (/) |
| 12 |
1
|
ackbij1lem9 |
|- ( ( (/) e. ( ~P _om i^i Fin ) /\ (/) e. ( ~P _om i^i Fin ) /\ ( (/) i^i (/) ) = (/) ) -> ( F ` ( (/) u. (/) ) ) = ( ( F ` (/) ) +o ( F ` (/) ) ) ) |
| 13 |
10 10 11 12
|
mp3an |
|- ( F ` ( (/) u. (/) ) ) = ( ( F ` (/) ) +o ( F ` (/) ) ) |
| 14 |
6 8 13
|
3eqtr2ri |
|- ( ( F ` (/) ) +o ( F ` (/) ) ) = ( ( F ` (/) ) +o (/) ) |
| 15 |
|
nnacan |
|- ( ( ( F ` (/) ) e. _om /\ ( F ` (/) ) e. _om /\ (/) e. _om ) -> ( ( ( F ` (/) ) +o ( F ` (/) ) ) = ( ( F ` (/) ) +o (/) ) <-> ( F ` (/) ) = (/) ) ) |
| 16 |
4 4 3 15
|
mp3an |
|- ( ( ( F ` (/) ) +o ( F ` (/) ) ) = ( ( F ` (/) ) +o (/) ) <-> ( F ` (/) ) = (/) ) |
| 17 |
14 16
|
mpbi |
|- ( F ` (/) ) = (/) |