Step |
Hyp |
Ref |
Expression |
1 |
|
fsuppun.f |
|- ( ph -> F finSupp Z ) |
2 |
|
fsuppun.g |
|- ( ph -> G finSupp Z ) |
3 |
|
fsuppimp |
|- ( F finSupp Z -> ( Fun F /\ ( F supp Z ) e. Fin ) ) |
4 |
|
fsuppimp |
|- ( G finSupp Z -> ( Fun G /\ ( G supp Z ) e. Fin ) ) |
5 |
|
unfi |
|- ( ( ( F supp Z ) e. Fin /\ ( G supp Z ) e. Fin ) -> ( ( F supp Z ) u. ( G supp Z ) ) e. Fin ) |
6 |
5
|
expcom |
|- ( ( G supp Z ) e. Fin -> ( ( F supp Z ) e. Fin -> ( ( F supp Z ) u. ( G supp Z ) ) e. Fin ) ) |
7 |
6
|
adantl |
|- ( ( Fun G /\ ( G supp Z ) e. Fin ) -> ( ( F supp Z ) e. Fin -> ( ( F supp Z ) u. ( G supp Z ) ) e. Fin ) ) |
8 |
2 4 7
|
3syl |
|- ( ph -> ( ( F supp Z ) e. Fin -> ( ( F supp Z ) u. ( G supp Z ) ) e. Fin ) ) |
9 |
8
|
com12 |
|- ( ( F supp Z ) e. Fin -> ( ph -> ( ( F supp Z ) u. ( G supp Z ) ) e. Fin ) ) |
10 |
3 9
|
simpl2im |
|- ( F finSupp Z -> ( ph -> ( ( F supp Z ) u. ( G supp Z ) ) e. Fin ) ) |
11 |
1 10
|
mpcom |
|- ( ph -> ( ( F supp Z ) u. ( G supp Z ) ) e. Fin ) |