Metamath Proof Explorer

Theorem fsuppunbi

Description: If the union of two classes/functions is a function, this union is finitely supported iff the two functions are finitely supported. (Contributed by AV, 18-Jun-2019)

Ref Expression
Hypothesis fsuppunbi.u 
|- ( ph -> Fun ( F u. G ) )
Assertion fsuppunbi 
|- ( ph -> ( ( F u. G ) finSupp Z <-> ( F finSupp Z /\ G finSupp Z ) ) )

Proof

Step Hyp Ref Expression
1 fsuppunbi.u 
 |-  ( ph -> Fun ( F u. G ) )
2 relfsupp 
 |-  Rel finSupp
3 2 brrelex12i 
 |-  ( ( F u. G ) finSupp Z -> ( ( F u. G ) e. _V /\ Z e. _V ) )
4 unexb 
 |-  ( ( F e. _V /\ G e. _V ) <-> ( F u. G ) e. _V )
5 simpr 
 |-  ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) -> ( ( F u. G ) supp Z ) e. Fin )
6 5 adantr 
 |-  ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> ( ( F u. G ) supp Z ) e. Fin )
7 simprlr 
 |-  ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> G e. _V )
8 7 suppun 
 |-  ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> ( F supp Z ) C_ ( ( F u. G ) supp Z ) )
9 6 8 ssfid 
 |-  ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> ( F supp Z ) e. Fin )
10 fununfun 
 |-  ( Fun ( F u. G ) -> ( Fun F /\ Fun G ) )
11 10 simpld 
 |-  ( Fun ( F u. G ) -> Fun F )
12 11 adantr 
 |-  ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) -> Fun F )
13 12 adantr 
 |-  ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> Fun F )
14 simprll 
 |-  ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> F e. _V )
15 simpr 
 |-  ( ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) -> Z e. _V )
16 15 adantl 
 |-  ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> Z e. _V )
17 funisfsupp 
 |-  ( ( Fun F /\ F e. _V /\ Z e. _V ) -> ( F finSupp Z <-> ( F supp Z ) e. Fin ) )
18 13 14 16 17 syl3anc 
 |-  ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> ( F finSupp Z <-> ( F supp Z ) e. Fin ) )
19 9 18 mpbird 
 |-  ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> F finSupp Z )
20 uncom 
 |-  ( F u. G ) = ( G u. F )
21 20 oveq1i 
 |-  ( ( F u. G ) supp Z ) = ( ( G u. F ) supp Z )
22 21 eleq1i 
 |-  ( ( ( F u. G ) supp Z ) e. Fin <-> ( ( G u. F ) supp Z ) e. Fin )
23 22 biimpi 
 |-  ( ( ( F u. G ) supp Z ) e. Fin -> ( ( G u. F ) supp Z ) e. Fin )
24 23 adantl 
 |-  ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) -> ( ( G u. F ) supp Z ) e. Fin )
25 24 adantr 
 |-  ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> ( ( G u. F ) supp Z ) e. Fin )
26 14 suppun 
 |-  ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> ( G supp Z ) C_ ( ( G u. F ) supp Z ) )
27 25 26 ssfid 
 |-  ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> ( G supp Z ) e. Fin )
28 10 simprd 
 |-  ( Fun ( F u. G ) -> Fun G )
29 28 adantr 
 |-  ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) -> Fun G )
30 29 adantr 
 |-  ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> Fun G )
31 funisfsupp 
 |-  ( ( Fun G /\ G e. _V /\ Z e. _V ) -> ( G finSupp Z <-> ( G supp Z ) e. Fin ) )
32 30 7 16 31 syl3anc 
 |-  ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> ( G finSupp Z <-> ( G supp Z ) e. Fin ) )
33 27 32 mpbird 
 |-  ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> G finSupp Z )
34 19 33 jca 
 |-  ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> ( F finSupp Z /\ G finSupp Z ) )
35 34 a1d 
 |-  ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> ( ph -> ( F finSupp Z /\ G finSupp Z ) ) )
36 35 ex 
 |-  ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) -> ( ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) -> ( ph -> ( F finSupp Z /\ G finSupp Z ) ) ) )
37 fsuppimp 
 |-  ( ( F u. G ) finSupp Z -> ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) )
38 36 37 syl11 
 |-  ( ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) -> ( ( F u. G ) finSupp Z -> ( ph -> ( F finSupp Z /\ G finSupp Z ) ) ) )
39 4 38 sylanbr 
 |-  ( ( ( F u. G ) e. _V /\ Z e. _V ) -> ( ( F u. G ) finSupp Z -> ( ph -> ( F finSupp Z /\ G finSupp Z ) ) ) )
40 3 39 mpcom 
 |-  ( ( F u. G ) finSupp Z -> ( ph -> ( F finSupp Z /\ G finSupp Z ) ) )
41 40 com12 
 |-  ( ph -> ( ( F u. G ) finSupp Z -> ( F finSupp Z /\ G finSupp Z ) ) )
42 simpl 
 |-  ( ( F finSupp Z /\ G finSupp Z ) -> F finSupp Z )
43 simpr 
 |-  ( ( F finSupp Z /\ G finSupp Z ) -> G finSupp Z )
44 42 43 fsuppun 
 |-  ( ( F finSupp Z /\ G finSupp Z ) -> ( ( F u. G ) supp Z ) e. Fin )
45 44 adantl 
 |-  ( ( ph /\ ( F finSupp Z /\ G finSupp Z ) ) -> ( ( F u. G ) supp Z ) e. Fin )
46 1 adantr 
 |-  ( ( ph /\ ( F finSupp Z /\ G finSupp Z ) ) -> Fun ( F u. G ) )
47 2 brrelex1i 
 |-  ( F finSupp Z -> F e. _V )
48 2 brrelex1i 
 |-  ( G finSupp Z -> G e. _V )
49 unexg 
 |-  ( ( F e. _V /\ G e. _V ) -> ( F u. G ) e. _V )
50 47 48 49 syl2an 
 |-  ( ( F finSupp Z /\ G finSupp Z ) -> ( F u. G ) e. _V )
51 50 adantl 
 |-  ( ( ph /\ ( F finSupp Z /\ G finSupp Z ) ) -> ( F u. G ) e. _V )
52 2 brrelex2i 
 |-  ( F finSupp Z -> Z e. _V )
53 52 adantr 
 |-  ( ( F finSupp Z /\ G finSupp Z ) -> Z e. _V )
54 53 adantl 
 |-  ( ( ph /\ ( F finSupp Z /\ G finSupp Z ) ) -> Z e. _V )
55 funisfsupp 
 |-  ( ( Fun ( F u. G ) /\ ( F u. G ) e. _V /\ Z e. _V ) -> ( ( F u. G ) finSupp Z <-> ( ( F u. G ) supp Z ) e. Fin ) )
56 46 51 54 55 syl3anc 
 |-  ( ( ph /\ ( F finSupp Z /\ G finSupp Z ) ) -> ( ( F u. G ) finSupp Z <-> ( ( F u. G ) supp Z ) e. Fin ) )
57 45 56 mpbird 
 |-  ( ( ph /\ ( F finSupp Z /\ G finSupp Z ) ) -> ( F u. G ) finSupp Z )
58 57 ex 
 |-  ( ph -> ( ( F finSupp Z /\ G finSupp Z ) -> ( F u. G ) finSupp Z ) )
59 41 58 impbid 
 |-  ( ph -> ( ( F u. G ) finSupp Z <-> ( F finSupp Z /\ G finSupp Z ) ) )