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 ( 𝐹𝐺 ) )
Assertion fsuppunbi ( 𝜑 → ( ( 𝐹𝐺 ) finSupp 𝑍 ↔ ( 𝐹 finSupp 𝑍𝐺 finSupp 𝑍 ) ) )

Proof

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