Metamath Proof Explorer

Theorem fsuppun

Description: The union of two finitely supported functions is finitely supported (but not necessarily a function!). (Contributed by AV, 3-Jun-2019)

Ref Expression
Hypotheses fsuppun.f 
|- ( ph -> F finSupp Z )
fsuppun.g 
|- ( ph -> G finSupp Z )
Assertion fsuppun 
|- ( ph -> ( ( F 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 cnvun 
 |-  `' ( F u. G ) = ( `' F u. `' G )
4 3 imaeq1i 
 |-  ( `' ( F u. G ) " ( _V \ { Z } ) ) = ( ( `' F u. `' G ) " ( _V \ { Z } ) )
5 imaundir 
 |-  ( ( `' F u. `' G ) " ( _V \ { Z } ) ) = ( ( `' F " ( _V \ { Z } ) ) u. ( `' G " ( _V \ { Z } ) ) )
6 4 5 eqtri 
 |-  ( `' ( F u. G ) " ( _V \ { Z } ) ) = ( ( `' F " ( _V \ { Z } ) ) u. ( `' G " ( _V \ { Z } ) ) )
7 unexb 
 |-  ( ( F e. _V /\ G e. _V ) <-> ( F u. G ) e. _V )
8 simpl 
 |-  ( ( F e. _V /\ G e. _V ) -> F e. _V )
9 7 8 sylbir 
 |-  ( ( F u. G ) e. _V -> F e. _V )
10 suppimacnv 
 |-  ( ( F e. _V /\ Z e. _V ) -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
11 9 10 sylan 
 |-  ( ( ( F u. G ) e. _V /\ Z e. _V ) -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
12 11 eqcomd 
 |-  ( ( ( F u. G ) e. _V /\ Z e. _V ) -> ( `' F " ( _V \ { Z } ) ) = ( F supp Z ) )
13 12 adantr 
 |-  ( ( ( ( F u. G ) e. _V /\ Z e. _V ) /\ ph ) -> ( `' F " ( _V \ { Z } ) ) = ( F supp Z ) )
14 1 fsuppimpd 
 |-  ( ph -> ( F supp Z ) e. Fin )
15 14 adantl 
 |-  ( ( ( ( F u. G ) e. _V /\ Z e. _V ) /\ ph ) -> ( F supp Z ) e. Fin )
16 13 15 eqeltrd 
 |-  ( ( ( ( F u. G ) e. _V /\ Z e. _V ) /\ ph ) -> ( `' F " ( _V \ { Z } ) ) e. Fin )
17 simpr 
 |-  ( ( F e. _V /\ G e. _V ) -> G e. _V )
18 7 17 sylbir 
 |-  ( ( F u. G ) e. _V -> G e. _V )
19 suppimacnv 
 |-  ( ( G e. _V /\ Z e. _V ) -> ( G supp Z ) = ( `' G " ( _V \ { Z } ) ) )
20 19 eqcomd 
 |-  ( ( G e. _V /\ Z e. _V ) -> ( `' G " ( _V \ { Z } ) ) = ( G supp Z ) )
21 18 20 sylan 
 |-  ( ( ( F u. G ) e. _V /\ Z e. _V ) -> ( `' G " ( _V \ { Z } ) ) = ( G supp Z ) )
22 21 adantr 
 |-  ( ( ( ( F u. G ) e. _V /\ Z e. _V ) /\ ph ) -> ( `' G " ( _V \ { Z } ) ) = ( G supp Z ) )
23 2 fsuppimpd 
 |-  ( ph -> ( G supp Z ) e. Fin )
24 23 adantl 
 |-  ( ( ( ( F u. G ) e. _V /\ Z e. _V ) /\ ph ) -> ( G supp Z ) e. Fin )
25 22 24 eqeltrd 
 |-  ( ( ( ( F u. G ) e. _V /\ Z e. _V ) /\ ph ) -> ( `' G " ( _V \ { Z } ) ) e. Fin )
26 unfi 
 |-  ( ( ( `' F " ( _V \ { Z } ) ) e. Fin /\ ( `' G " ( _V \ { Z } ) ) e. Fin ) -> ( ( `' F " ( _V \ { Z } ) ) u. ( `' G " ( _V \ { Z } ) ) ) e. Fin )
27 16 25 26 syl2anc 
 |-  ( ( ( ( F u. G ) e. _V /\ Z e. _V ) /\ ph ) -> ( ( `' F " ( _V \ { Z } ) ) u. ( `' G " ( _V \ { Z } ) ) ) e. Fin )
28 6 27 eqeltrid 
 |-  ( ( ( ( F u. G ) e. _V /\ Z e. _V ) /\ ph ) -> ( `' ( F u. G ) " ( _V \ { Z } ) ) e. Fin )
29 suppimacnv 
 |-  ( ( ( F u. G ) e. _V /\ Z e. _V ) -> ( ( F u. G ) supp Z ) = ( `' ( F u. G ) " ( _V \ { Z } ) ) )
30 29 eleq1d 
 |-  ( ( ( F u. G ) e. _V /\ Z e. _V ) -> ( ( ( F u. G ) supp Z ) e. Fin <-> ( `' ( F u. G ) " ( _V \ { Z } ) ) e. Fin ) )
31 30 adantr 
 |-  ( ( ( ( F u. G ) e. _V /\ Z e. _V ) /\ ph ) -> ( ( ( F u. G ) supp Z ) e. Fin <-> ( `' ( F u. G ) " ( _V \ { Z } ) ) e. Fin ) )
32 28 31 mpbird 
 |-  ( ( ( ( F u. G ) e. _V /\ Z e. _V ) /\ ph ) -> ( ( F u. G ) supp Z ) e. Fin )
33 32 ex 
 |-  ( ( ( F u. G ) e. _V /\ Z e. _V ) -> ( ph -> ( ( F u. G ) supp Z ) e. Fin ) )
34 supp0prc 
 |-  ( -. ( ( F u. G ) e. _V /\ Z e. _V ) -> ( ( F u. G ) supp Z ) = (/) )
35 0fin 
 |-  (/) e. Fin
36 34 35 eqeltrdi 
 |-  ( -. ( ( F u. G ) e. _V /\ Z e. _V ) -> ( ( F u. G ) supp Z ) e. Fin )
37 36 a1d 
 |-  ( -. ( ( F u. G ) e. _V /\ Z e. _V ) -> ( ph -> ( ( F u. G ) supp Z ) e. Fin ) )
38 33 37 pm2.61i 
 |-  ( ph -> ( ( F u. G ) supp Z ) e. Fin )