Metamath Proof Explorer


Theorem ackbij1lem8

Description: Lemma for ackbij1 . (Contributed by Stefan O'Rear, 19-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 ackbij1lem8
|- ( A e. _om -> ( F ` { A } ) = ( card ` ~P A ) )

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 sneq
 |-  ( a = A -> { a } = { A } )
3 2 fveq2d
 |-  ( a = A -> ( F ` { a } ) = ( F ` { A } ) )
4 pweq
 |-  ( a = A -> ~P a = ~P A )
5 4 fveq2d
 |-  ( a = A -> ( card ` ~P a ) = ( card ` ~P A ) )
6 3 5 eqeq12d
 |-  ( a = A -> ( ( F ` { a } ) = ( card ` ~P a ) <-> ( F ` { A } ) = ( card ` ~P A ) ) )
7 ackbij1lem4
 |-  ( a e. _om -> { a } e. ( ~P _om i^i Fin ) )
8 1 ackbij1lem7
 |-  ( { a } e. ( ~P _om i^i Fin ) -> ( F ` { a } ) = ( card ` U_ y e. { a } ( { y } X. ~P y ) ) )
9 7 8 syl
 |-  ( a e. _om -> ( F ` { a } ) = ( card ` U_ y e. { a } ( { y } X. ~P y ) ) )
10 vex
 |-  a e. _V
11 sneq
 |-  ( y = a -> { y } = { a } )
12 pweq
 |-  ( y = a -> ~P y = ~P a )
13 11 12 xpeq12d
 |-  ( y = a -> ( { y } X. ~P y ) = ( { a } X. ~P a ) )
14 10 13 iunxsn
 |-  U_ y e. { a } ( { y } X. ~P y ) = ( { a } X. ~P a )
15 14 fveq2i
 |-  ( card ` U_ y e. { a } ( { y } X. ~P y ) ) = ( card ` ( { a } X. ~P a ) )
16 vpwex
 |-  ~P a e. _V
17 xpsnen2g
 |-  ( ( a e. _V /\ ~P a e. _V ) -> ( { a } X. ~P a ) ~~ ~P a )
18 10 16 17 mp2an
 |-  ( { a } X. ~P a ) ~~ ~P a
19 carden2b
 |-  ( ( { a } X. ~P a ) ~~ ~P a -> ( card ` ( { a } X. ~P a ) ) = ( card ` ~P a ) )
20 18 19 ax-mp
 |-  ( card ` ( { a } X. ~P a ) ) = ( card ` ~P a )
21 15 20 eqtri
 |-  ( card ` U_ y e. { a } ( { y } X. ~P y ) ) = ( card ` ~P a )
22 9 21 eqtrdi
 |-  ( a e. _om -> ( F ` { a } ) = ( card ` ~P a ) )
23 6 22 vtoclga
 |-  ( A e. _om -> ( F ` { A } ) = ( card ` ~P A ) )