Metamath Proof Explorer

Theorem ackbij1lem9

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 ackbij1lem9 
|- ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> ( F ` ( A u. B ) ) = ( ( F ` A ) +o ( F ` B ) ) )

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 
 |-  ( A e. ( ~P _om i^i Fin ) -> A e. Fin )
3 2 3ad2ant1 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> A e. Fin )
4 snfi 
 |-  { y } e. Fin
5 elinel1 
 |-  ( A e. ( ~P _om i^i Fin ) -> A e. ~P _om )
6 5 elpwid 
 |-  ( A e. ( ~P _om i^i Fin ) -> A C_ _om )
7 6 3ad2ant1 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> A C_ _om )
8 onfin2 
 |-  _om = ( On i^i Fin )
9 inss2 
 |-  ( On i^i Fin ) C_ Fin
10 8 9 eqsstri 
 |-  _om C_ Fin
11 7 10 sstrdi 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> A C_ Fin )
12 11 sselda 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) /\ y e. A ) -> y e. Fin )
13 pwfi 
 |-  ( y e. Fin <-> ~P y e. Fin )
14 12 13 sylib 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) /\ y e. A ) -> ~P y e. Fin )
15 xpfi 
 |-  ( ( { y } e. Fin /\ ~P y e. Fin ) -> ( { y } X. ~P y ) e. Fin )
16 4 14 15 sylancr 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) /\ y e. A ) -> ( { y } X. ~P y ) e. Fin )
17 16 ralrimiva 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> A. y e. A ( { y } X. ~P y ) e. Fin )
18 iunfi 
 |-  ( ( A e. Fin /\ A. y e. A ( { y } X. ~P y ) e. Fin ) -> U_ y e. A ( { y } X. ~P y ) e. Fin )
19 3 17 18 syl2anc 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> U_ y e. A ( { y } X. ~P y ) e. Fin )
20 ficardid 
 |-  ( U_ y e. A ( { y } X. ~P y ) e. Fin -> ( card ` U_ y e. A ( { y } X. ~P y ) ) ~~ U_ y e. A ( { y } X. ~P y ) )
21 19 20 syl 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> ( card ` U_ y e. A ( { y } X. ~P y ) ) ~~ U_ y e. A ( { y } X. ~P y ) )
22 elinel2 
 |-  ( B e. ( ~P _om i^i Fin ) -> B e. Fin )
23 22 3ad2ant2 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> B e. Fin )
24 elinel1 
 |-  ( B e. ( ~P _om i^i Fin ) -> B e. ~P _om )
25 24 elpwid 
 |-  ( B e. ( ~P _om i^i Fin ) -> B C_ _om )
26 25 3ad2ant2 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> B C_ _om )
27 26 10 sstrdi 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> B C_ Fin )
28 27 sselda 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) /\ y e. B ) -> y e. Fin )
29 28 13 sylib 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) /\ y e. B ) -> ~P y e. Fin )
30 4 29 15 sylancr 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) /\ y e. B ) -> ( { y } X. ~P y ) e. Fin )
31 30 ralrimiva 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> A. y e. B ( { y } X. ~P y ) e. Fin )
32 iunfi 
 |-  ( ( B e. Fin /\ A. y e. B ( { y } X. ~P y ) e. Fin ) -> U_ y e. B ( { y } X. ~P y ) e. Fin )
33 23 31 32 syl2anc 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> U_ y e. B ( { y } X. ~P y ) e. Fin )
34 ficardid 
 |-  ( U_ y e. B ( { y } X. ~P y ) e. Fin -> ( card ` U_ y e. B ( { y } X. ~P y ) ) ~~ U_ y e. B ( { y } X. ~P y ) )
35 33 34 syl 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> ( card ` U_ y e. B ( { y } X. ~P y ) ) ~~ U_ y e. B ( { y } X. ~P y ) )
36 djuen 
 |-  ( ( ( card ` U_ y e. A ( { y } X. ~P y ) ) ~~ U_ y e. A ( { y } X. ~P y ) /\ ( card ` U_ y e. B ( { y } X. ~P y ) ) ~~ U_ y e. B ( { y } X. ~P y ) ) -> ( ( card ` U_ y e. A ( { y } X. ~P y ) ) |_| ( card ` U_ y e. B ( { y } X. ~P y ) ) ) ~~ ( U_ y e. A ( { y } X. ~P y ) |_| U_ y e. B ( { y } X. ~P y ) ) )
37 21 35 36 syl2anc 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> ( ( card ` U_ y e. A ( { y } X. ~P y ) ) |_| ( card ` U_ y e. B ( { y } X. ~P y ) ) ) ~~ ( U_ y e. A ( { y } X. ~P y ) |_| U_ y e. B ( { y } X. ~P y ) ) )
38 djudisj 
 |-  ( ( A i^i B ) = (/) -> ( U_ y e. A ( { y } X. ~P y ) i^i U_ y e. B ( { y } X. ~P y ) ) = (/) )
39 38 3ad2ant3 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> ( U_ y e. A ( { y } X. ~P y ) i^i U_ y e. B ( { y } X. ~P y ) ) = (/) )
40 endjudisj 
 |-  ( ( U_ y e. A ( { y } X. ~P y ) e. Fin /\ U_ y e. B ( { y } X. ~P y ) e. Fin /\ ( U_ y e. A ( { y } X. ~P y ) i^i U_ y e. B ( { y } X. ~P y ) ) = (/) ) -> ( U_ y e. A ( { y } X. ~P y ) |_| U_ y e. B ( { y } X. ~P y ) ) ~~ ( U_ y e. A ( { y } X. ~P y ) u. U_ y e. B ( { y } X. ~P y ) ) )
41 19 33 39 40 syl3anc 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> ( U_ y e. A ( { y } X. ~P y ) |_| U_ y e. B ( { y } X. ~P y ) ) ~~ ( U_ y e. A ( { y } X. ~P y ) u. U_ y e. B ( { y } X. ~P y ) ) )
42 iunxun 
 |-  U_ y e. ( A u. B ) ( { y } X. ~P y ) = ( U_ y e. A ( { y } X. ~P y ) u. U_ y e. B ( { y } X. ~P y ) )
43 41 42 breqtrrdi 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> ( U_ y e. A ( { y } X. ~P y ) |_| U_ y e. B ( { y } X. ~P y ) ) ~~ U_ y e. ( A u. B ) ( { y } X. ~P y ) )
44 entr 
 |-  ( ( ( ( card ` U_ y e. A ( { y } X. ~P y ) ) |_| ( card ` U_ y e. B ( { y } X. ~P y ) ) ) ~~ ( U_ y e. A ( { y } X. ~P y ) |_| U_ y e. B ( { y } X. ~P y ) ) /\ ( U_ y e. A ( { y } X. ~P y ) |_| U_ y e. B ( { y } X. ~P y ) ) ~~ U_ y e. ( A u. B ) ( { y } X. ~P y ) ) -> ( ( card ` U_ y e. A ( { y } X. ~P y ) ) |_| ( card ` U_ y e. B ( { y } X. ~P y ) ) ) ~~ U_ y e. ( A u. B ) ( { y } X. ~P y ) )
45 37 43 44 syl2anc 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> ( ( card ` U_ y e. A ( { y } X. ~P y ) ) |_| ( card ` U_ y e. B ( { y } X. ~P y ) ) ) ~~ U_ y e. ( A u. B ) ( { y } X. ~P y ) )
46 carden2b 
 |-  ( ( ( card ` U_ y e. A ( { y } X. ~P y ) ) |_| ( card ` U_ y e. B ( { y } X. ~P y ) ) ) ~~ U_ y e. ( A u. B ) ( { y } X. ~P y ) -> ( card ` ( ( card ` U_ y e. A ( { y } X. ~P y ) ) |_| ( card ` U_ y e. B ( { y } X. ~P y ) ) ) ) = ( card ` U_ y e. ( A u. B ) ( { y } X. ~P y ) ) )
47 45 46 syl 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> ( card ` ( ( card ` U_ y e. A ( { y } X. ~P y ) ) |_| ( card ` U_ y e. B ( { y } X. ~P y ) ) ) ) = ( card ` U_ y e. ( A u. B ) ( { y } X. ~P y ) ) )
48 ficardom 
 |-  ( U_ y e. A ( { y } X. ~P y ) e. Fin -> ( card ` U_ y e. A ( { y } X. ~P y ) ) e. _om )
49 19 48 syl 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> ( card ` U_ y e. A ( { y } X. ~P y ) ) e. _om )
50 ficardom 
 |-  ( U_ y e. B ( { y } X. ~P y ) e. Fin -> ( card ` U_ y e. B ( { y } X. ~P y ) ) e. _om )
51 33 50 syl 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> ( card ` U_ y e. B ( { y } X. ~P y ) ) e. _om )
52 nnadju 
 |-  ( ( ( card ` U_ y e. A ( { y } X. ~P y ) ) e. _om /\ ( card ` U_ y e. B ( { y } X. ~P y ) ) e. _om ) -> ( card ` ( ( card ` U_ y e. A ( { y } X. ~P y ) ) |_| ( card ` U_ y e. B ( { y } X. ~P y ) ) ) ) = ( ( card ` U_ y e. A ( { y } X. ~P y ) ) +o ( card ` U_ y e. B ( { y } X. ~P y ) ) ) )
53 49 51 52 syl2anc 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> ( card ` ( ( card ` U_ y e. A ( { y } X. ~P y ) ) |_| ( card ` U_ y e. B ( { y } X. ~P y ) ) ) ) = ( ( card ` U_ y e. A ( { y } X. ~P y ) ) +o ( card ` U_ y e. B ( { y } X. ~P y ) ) ) )
54 47 53 eqtr3d 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> ( card ` U_ y e. ( A u. B ) ( { y } X. ~P y ) ) = ( ( card ` U_ y e. A ( { y } X. ~P y ) ) +o ( card ` U_ y e. B ( { y } X. ~P y ) ) ) )
55 ackbij1lem6 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( A u. B ) e. ( ~P _om i^i Fin ) )
56 55 3adant3 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> ( A u. B ) e. ( ~P _om i^i Fin ) )
57 1 ackbij1lem7 
 |-  ( ( A u. B ) e. ( ~P _om i^i Fin ) -> ( F ` ( A u. B ) ) = ( card ` U_ y e. ( A u. B ) ( { y } X. ~P y ) ) )
58 56 57 syl 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> ( F ` ( A u. B ) ) = ( card ` U_ y e. ( A u. B ) ( { y } X. ~P y ) ) )
59 1 ackbij1lem7 
 |-  ( A e. ( ~P _om i^i Fin ) -> ( F ` A ) = ( card ` U_ y e. A ( { y } X. ~P y ) ) )
60 1 ackbij1lem7 
 |-  ( B e. ( ~P _om i^i Fin ) -> ( F ` B ) = ( card ` U_ y e. B ( { y } X. ~P y ) ) )
61 59 60 oveqan12d 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( ( F ` A ) +o ( F ` B ) ) = ( ( card ` U_ y e. A ( { y } X. ~P y ) ) +o ( card ` U_ y e. B ( { y } X. ~P y ) ) ) )
62 61 3adant3 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> ( ( F ` A ) +o ( F ` B ) ) = ( ( card ` U_ y e. A ( { y } X. ~P y ) ) +o ( card ` U_ y e. B ( { y } X. ~P y ) ) ) )
63 54 58 62 3eqtr4d 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) /\ ( A i^i B ) = (/) ) -> ( F ` ( A u. B ) ) = ( ( F ` A ) +o ( F ` B ) ) )