Theorem ffsuppbi

Description: Two ways of saying that a function with known codomain is finitely supported. (Contributed by AV, 8-Jul-2019)

	Ref	Expression
Assertion	ffsuppbi	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 : 𝐼 ⟶ 𝑆 → ( 𝐹 finSupp 𝑍 ↔ ( ◡ 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) ∈ Fin ) ) )

Proof

Step	Hyp	Ref	Expression
1		ffun	⊢ ( 𝐹 : 𝐼 ⟶ 𝑆 → Fun 𝐹 )
2	1	adantl	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐹 : 𝐼 ⟶ 𝑆 ) → Fun 𝐹 )
3		fex	⊢ ( ( 𝐹 : 𝐼 ⟶ 𝑆 ∧ 𝐼 ∈ 𝑉 ) → 𝐹 ∈ V )
4	3	expcom	⊢ ( 𝐼 ∈ 𝑉 → ( 𝐹 : 𝐼 ⟶ 𝑆 → 𝐹 ∈ V ) )
5	4	adantr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 : 𝐼 ⟶ 𝑆 → 𝐹 ∈ V ) )
6	5	imp	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐹 : 𝐼 ⟶ 𝑆 ) → 𝐹 ∈ V )
7		simplr	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐹 : 𝐼 ⟶ 𝑆 ) → 𝑍 ∈ 𝑊 )
8		funisfsupp	⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ V ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
9	2 6 7 8	syl3anc	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐹 : 𝐼 ⟶ 𝑆 ) → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
10		fsuppeq	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 : 𝐼 ⟶ 𝑆 → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) ) )
11	10	imp	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐹 : 𝐼 ⟶ 𝑆 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) )
12	11	eleq1d	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐹 : 𝐼 ⟶ 𝑆 ) → ( ( 𝐹 supp 𝑍 ) ∈ Fin ↔ ( ◡ 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) ∈ Fin ) )
13	9 12	bitrd	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐹 : 𝐼 ⟶ 𝑆 ) → ( 𝐹 finSupp 𝑍 ↔ ( ◡ 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) ∈ Fin ) )
14	13	ex	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 : 𝐼 ⟶ 𝑆 → ( 𝐹 finSupp 𝑍 ↔ ( ◡ 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) ∈ Fin ) ) )