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 ) ) )