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