Metamath Proof Explorer

Theorem ackbij1lem13

Description: Lemma for ackbij1 . (Contributed by Stefan O'Rear, 18-Nov-2014)

Ref Expression
Hypothesis ackbij.f 
|- F = ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ y e. x ( { y } X. ~P y ) ) )
Assertion ackbij1lem13 
|- ( F ` (/) ) = (/)

Proof

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 ` (/) ) = (/)