Theorem fsuppco

Description: The composition of a 1-1 function with a finitely supported function is finitely supported. (Contributed by AV, 28-May-2019)

	Ref	Expression
Hypotheses	fsuppco.f	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )
	fsuppco.g	⊢ ( 𝜑 → 𝐺 : 𝑋 –1-1→ 𝑌 )
	fsuppco.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
	fsuppco.v	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
Assertion	fsuppco	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) finSupp 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		fsuppco.f	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )
2		fsuppco.g	⊢ ( 𝜑 → 𝐺 : 𝑋 –1-1→ 𝑌 )
3		fsuppco.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
4		fsuppco.v	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
5		df-f1	⊢ ( 𝐺 : 𝑋 –1-1→ 𝑌 ↔ ( 𝐺 : 𝑋 ⟶ 𝑌 ∧ Fun ◡ 𝐺 ) )
6	5	simprbi	⊢ ( 𝐺 : 𝑋 –1-1→ 𝑌 → Fun ◡ 𝐺 )
7	2 6	syl	⊢ ( 𝜑 → Fun ◡ 𝐺 )
8		cofunex2g	⊢ ( ( 𝐹 ∈ 𝑉 ∧ Fun ◡ 𝐺 ) → ( 𝐹 ∘ 𝐺 ) ∈ V )
9	4 7 8	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) ∈ V )
10		suppimacnv	⊢ ( ( ( 𝐹 ∘ 𝐺 ) ∈ V ∧ 𝑍 ∈ 𝑊 ) → ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) = ( ◡ ( 𝐹 ∘ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) )
11	9 3 10	syl2anc	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) = ( ◡ ( 𝐹 ∘ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) )
12		suppimacnv	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
13	4 3 12	syl2anc	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
14	1	fsuppimpd	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )
15	13 14	eqeltrrd	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∈ Fin )
16	15 2	fsuppcolem	⊢ ( 𝜑 → ( ◡ ( 𝐹 ∘ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) ∈ Fin )
17	11 16	eqeltrd	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) ∈ Fin )
18		fsuppimp	⊢ ( 𝐹 finSupp 𝑍 → ( Fun 𝐹 ∧ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
19	18	simpld	⊢ ( 𝐹 finSupp 𝑍 → Fun 𝐹 )
20	1 19	syl	⊢ ( 𝜑 → Fun 𝐹 )
21		f1fun	⊢ ( 𝐺 : 𝑋 –1-1→ 𝑌 → Fun 𝐺 )
22	2 21	syl	⊢ ( 𝜑 → Fun 𝐺 )
23		funco	⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ) → Fun ( 𝐹 ∘ 𝐺 ) )
24	20 22 23	syl2anc	⊢ ( 𝜑 → Fun ( 𝐹 ∘ 𝐺 ) )
25		funisfsupp	⊢ ( ( Fun ( 𝐹 ∘ 𝐺 ) ∧ ( 𝐹 ∘ 𝐺 ) ∈ V ∧ 𝑍 ∈ 𝑊 ) → ( ( 𝐹 ∘ 𝐺 ) finSupp 𝑍 ↔ ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) ∈ Fin ) )
26	24 9 3 25	syl3anc	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐺 ) finSupp 𝑍 ↔ ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) ∈ Fin ) )
27	17 26	mpbird	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) finSupp 𝑍 )