This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )