Metamath Proof Explorer


Theorem ackbij1lem10

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 ackbij1lem10
|- F : ( ~P _om i^i Fin ) --> _om

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 elinel2
 |-  ( x e. ( ~P _om i^i Fin ) -> x e. Fin )
3 snfi
 |-  { y } e. Fin
4 elinel1
 |-  ( x e. ( ~P _om i^i Fin ) -> x e. ~P _om )
5 4 elpwid
 |-  ( x e. ( ~P _om i^i Fin ) -> x C_ _om )
6 onfin2
 |-  _om = ( On i^i Fin )
7 inss2
 |-  ( On i^i Fin ) C_ Fin
8 6 7 eqsstri
 |-  _om C_ Fin
9 5 8 sstrdi
 |-  ( x e. ( ~P _om i^i Fin ) -> x C_ Fin )
10 9 sselda
 |-  ( ( x e. ( ~P _om i^i Fin ) /\ y e. x ) -> y e. Fin )
11 pwfi
 |-  ( y e. Fin <-> ~P y e. Fin )
12 10 11 sylib
 |-  ( ( x e. ( ~P _om i^i Fin ) /\ y e. x ) -> ~P y e. Fin )
13 xpfi
 |-  ( ( { y } e. Fin /\ ~P y e. Fin ) -> ( { y } X. ~P y ) e. Fin )
14 3 12 13 sylancr
 |-  ( ( x e. ( ~P _om i^i Fin ) /\ y e. x ) -> ( { y } X. ~P y ) e. Fin )
15 14 ralrimiva
 |-  ( x e. ( ~P _om i^i Fin ) -> A. y e. x ( { y } X. ~P y ) e. Fin )
16 iunfi
 |-  ( ( x e. Fin /\ A. y e. x ( { y } X. ~P y ) e. Fin ) -> U_ y e. x ( { y } X. ~P y ) e. Fin )
17 2 15 16 syl2anc
 |-  ( x e. ( ~P _om i^i Fin ) -> U_ y e. x ( { y } X. ~P y ) e. Fin )
18 ficardom
 |-  ( U_ y e. x ( { y } X. ~P y ) e. Fin -> ( card ` U_ y e. x ( { y } X. ~P y ) ) e. _om )
19 17 18 syl
 |-  ( x e. ( ~P _om i^i Fin ) -> ( card ` U_ y e. x ( { y } X. ~P y ) ) e. _om )
20 1 19 fmpti
 |-  F : ( ~P _om i^i Fin ) --> _om