Step |
Hyp |
Ref |
Expression |
1 |
|
qshash.1 |
|- ( ph -> .~ Er A ) |
2 |
|
qshash.2 |
|- ( ph -> A e. Fin ) |
3 |
|
erex |
|- ( .~ Er A -> ( A e. Fin -> .~ e. _V ) ) |
4 |
1 2 3
|
sylc |
|- ( ph -> .~ e. _V ) |
5 |
1 4
|
uniqs2 |
|- ( ph -> U. ( A /. .~ ) = A ) |
6 |
5
|
fveq2d |
|- ( ph -> ( # ` U. ( A /. .~ ) ) = ( # ` A ) ) |
7 |
|
pwfi |
|- ( A e. Fin <-> ~P A e. Fin ) |
8 |
2 7
|
sylib |
|- ( ph -> ~P A e. Fin ) |
9 |
1
|
qsss |
|- ( ph -> ( A /. .~ ) C_ ~P A ) |
10 |
8 9
|
ssfid |
|- ( ph -> ( A /. .~ ) e. Fin ) |
11 |
|
elpwi |
|- ( x e. ~P A -> x C_ A ) |
12 |
|
ssfi |
|- ( ( A e. Fin /\ x C_ A ) -> x e. Fin ) |
13 |
12
|
ex |
|- ( A e. Fin -> ( x C_ A -> x e. Fin ) ) |
14 |
2 11 13
|
syl2im |
|- ( ph -> ( x e. ~P A -> x e. Fin ) ) |
15 |
14
|
ssrdv |
|- ( ph -> ~P A C_ Fin ) |
16 |
9 15
|
sstrd |
|- ( ph -> ( A /. .~ ) C_ Fin ) |
17 |
|
qsdisj2 |
|- ( .~ Er A -> Disj_ x e. ( A /. .~ ) x ) |
18 |
1 17
|
syl |
|- ( ph -> Disj_ x e. ( A /. .~ ) x ) |
19 |
10 16 18
|
hashuni |
|- ( ph -> ( # ` U. ( A /. .~ ) ) = sum_ x e. ( A /. .~ ) ( # ` x ) ) |
20 |
6 19
|
eqtr3d |
|- ( ph -> ( # ` A ) = sum_ x e. ( A /. .~ ) ( # ` x ) ) |