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	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )
	fsuppun.g	⊢ ( 𝜑 → 𝐺 finSupp 𝑍 )
Assertion	fsuppun	⊢ ( 𝜑 → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		fsuppun.f	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )
2		fsuppun.g	⊢ ( 𝜑 → 𝐺 finSupp 𝑍 )
3		cnvun	⊢ ◡ ( 𝐹 ∪ 𝐺 ) = ( ◡ 𝐹 ∪ ◡ 𝐺 )
4	3	imaeq1i	⊢ ( ◡ ( 𝐹 ∪ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) = ( ( ◡ 𝐹 ∪ ◡ 𝐺 ) “ ( V ∖ { 𝑍 } ) )
5		imaundir	⊢ ( ( ◡ 𝐹 ∪ ◡ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) = ( ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∪ ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) )
6	4 5	eqtri	⊢ ( ◡ ( 𝐹 ∪ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) = ( ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∪ ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) )
7		unexb	⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ↔ ( 𝐹 ∪ 𝐺 ) ∈ V )
8		simpl	⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → 𝐹 ∈ V )
9	7 8	sylbir	⊢ ( ( 𝐹 ∪ 𝐺 ) ∈ V → 𝐹 ∈ V )
10		suppimacnv	⊢ ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
11	9 10	sylan	⊢ ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
12	11	eqcomd	⊢ ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) = ( 𝐹 supp 𝑍 ) )
13	12	adantr	⊢ ( ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) = ( 𝐹 supp 𝑍 ) )
14	1	fsuppimpd	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )
15	14	adantl	⊢ ( ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( 𝐹 supp 𝑍 ) ∈ Fin )
16	13 15	eqeltrd	⊢ ( ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∈ Fin )
17		simpr	⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → 𝐺 ∈ V )
18	7 17	sylbir	⊢ ( ( 𝐹 ∪ 𝐺 ) ∈ V → 𝐺 ∈ V )
19		suppimacnv	⊢ ( ( 𝐺 ∈ V ∧ 𝑍 ∈ V ) → ( 𝐺 supp 𝑍 ) = ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) )
20	19	eqcomd	⊢ ( ( 𝐺 ∈ V ∧ 𝑍 ∈ V ) → ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) = ( 𝐺 supp 𝑍 ) )
21	18 20	sylan	⊢ ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) = ( 𝐺 supp 𝑍 ) )
22	21	adantr	⊢ ( ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) = ( 𝐺 supp 𝑍 ) )
23	2	fsuppimpd	⊢ ( 𝜑 → ( 𝐺 supp 𝑍 ) ∈ Fin )
24	23	adantl	⊢ ( ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( 𝐺 supp 𝑍 ) ∈ Fin )
25	22 24	eqeltrd	⊢ ( ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) ∈ Fin )
26		unfi	⊢ ( ( ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∈ Fin ∧ ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) ∈ Fin ) → ( ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∪ ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) ) ∈ Fin )
27	16 25 26	syl2anc	⊢ ( ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∪ ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) ) ∈ Fin )
28	6 27	eqeltrid	⊢ ( ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ◡ ( 𝐹 ∪ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) ∈ Fin )
29		suppimacnv	⊢ ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) = ( ◡ ( 𝐹 ∪ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) )
30	29	eleq1d	⊢ ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ↔ ( ◡ ( 𝐹 ∪ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) ∈ Fin ) )
31	30	adantr	⊢ ( ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ↔ ( ◡ ( 𝐹 ∪ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) ∈ Fin ) )
32	28 31	mpbird	⊢ ( ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin )
33	32	ex	⊢ ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( 𝜑 → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) )
34		supp0prc	⊢ ( ¬ ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) = ∅ )
35		0fin	⊢ ∅ ∈ Fin
36	34 35	eqeltrdi	⊢ ( ¬ ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin )
37	36	a1d	⊢ ( ¬ ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( 𝜑 → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) )
38	33 37	pm2.61i	⊢ ( 𝜑 → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin )