Metamath Proof Explorer


Theorem fsuppunfi

Description: The union of the support of two finitely supported functions is finite. (Contributed by AV, 1-Jul-2019)

Ref Expression
Hypotheses fsuppun.f
|- ( ph -> F finSupp Z )
fsuppun.g
|- ( ph -> G finSupp Z )
Assertion fsuppunfi
|- ( ph -> ( ( F supp Z ) u. ( G supp Z ) ) e. Fin )

Proof

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 )