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 bilani ⊢ ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) → ( ( 𝐺 ∪ 𝐹 ) supp 𝑍 ) ∈ Fin )
24 23 adantr ⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → ( ( 𝐺 ∪ 𝐹 ) supp 𝑍 ) ∈ Fin )
25 14 suppun ⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → ( 𝐺 supp 𝑍 ) ⊆ ( ( 𝐺 ∪ 𝐹 ) supp 𝑍 ) )
26 24 25 ssfid ⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → ( 𝐺 supp 𝑍 ) ∈ Fin )
27 10 simprd ⊢ ( Fun ( 𝐹 ∪ 𝐺 ) → Fun 𝐺 )
28 27 adantr ⊢ ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) → Fun 𝐺 )
29 28 adantr ⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → Fun 𝐺 )
30 funisfsupp ⊢ ( ( Fun 𝐺 ∧ 𝐺 ∈ V ∧ 𝑍 ∈ V ) → ( 𝐺 finSupp 𝑍 ↔ ( 𝐺 supp 𝑍 ) ∈ Fin ) )
31 29 7 16 30 syl3anc ⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → ( 𝐺 finSupp 𝑍 ↔ ( 𝐺 supp 𝑍 ) ∈ Fin ) )
32 26 31 mpbird ⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → 𝐺 finSupp 𝑍 )
33 19 32 jca ⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) )
34 33 a1d ⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → ( 𝜑 → ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) )
35 34 ex ⊢ ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) → ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) → ( 𝜑 → ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) ) )
36 fsuppimp ⊢ ( ( 𝐹 ∪ 𝐺 ) finSupp 𝑍 → ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) )
37 35 36 syl11 ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) → ( ( 𝐹 ∪ 𝐺 ) finSupp 𝑍 → ( 𝜑 → ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) ) )
38 4 37 sylanbr ⊢ ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝐹 ∪ 𝐺 ) finSupp 𝑍 → ( 𝜑 → ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) ) )
39 3 38 mpcom ⊢ ( ( 𝐹 ∪ 𝐺 ) finSupp 𝑍 → ( 𝜑 → ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) )
40 39 com12 ⊢ ( 𝜑 → ( ( 𝐹 ∪ 𝐺 ) finSupp 𝑍 → ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) )
41 simpl ⊢ ( ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) → 𝐹 finSupp 𝑍 )
42 simpr ⊢ ( ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) → 𝐺 finSupp 𝑍 )
43 41 42 fsuppun ⊢ ( ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin )
44 43 adantl ⊢ ( ( 𝜑 ∧ ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin )
45 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) → Fun ( 𝐹 ∪ 𝐺 ) )
46 2 brrelex1i ⊢ ( 𝐹 finSupp 𝑍 → 𝐹 ∈ V )
47 2 brrelex1i ⊢ ( 𝐺 finSupp 𝑍 → 𝐺 ∈ V )
48 unexg ⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 𝐹 ∪ 𝐺 ) ∈ V )
49 46 47 48 syl2an ⊢ ( ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) → ( 𝐹 ∪ 𝐺 ) ∈ V )
50 49 adantl ⊢ ( ( 𝜑 ∧ ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) → ( 𝐹 ∪ 𝐺 ) ∈ V )
51 2 brrelex2i ⊢ ( 𝐹 finSupp 𝑍 → 𝑍 ∈ V )
52 51 adantr ⊢ ( ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) → 𝑍 ∈ V )
53 52 adantl ⊢ ( ( 𝜑 ∧ ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) → 𝑍 ∈ V )
54 funisfsupp ⊢ ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝐹 ∪ 𝐺 ) finSupp 𝑍 ↔ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) )
55 45 50 53 54 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) → ( ( 𝐹 ∪ 𝐺 ) finSupp 𝑍 ↔ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) )
56 44 55 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) → ( 𝐹 ∪ 𝐺 ) finSupp 𝑍 )
57 56 ex ⊢ ( 𝜑 → ( ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) → ( 𝐹 ∪ 𝐺 ) finSupp 𝑍 ) )
58 40 57 impbid ⊢ ( 𝜑 → ( ( 𝐹 ∪ 𝐺 ) finSupp 𝑍 ↔ ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) )