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 φ Fun F G
Assertion fsuppunbi φ finSupp Z F G finSupp Z F finSupp Z G

Proof

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