Theorem funisfsupp

Description: The property of a function to be finitely supported (in relation to a given zero). (Contributed by AV, 23-May-2019)

	Ref	Expression
Assertion	funisfsupp	⊢ ( ( Fun 𝑅 ∧ 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑅 finSupp 𝑍 ↔ ( 𝑅 supp 𝑍 ) ∈ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		isfsupp	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑅 finSupp 𝑍 ↔ ( Fun 𝑅 ∧ ( 𝑅 supp 𝑍 ) ∈ Fin ) ) )
2	1	3adant1	⊢ ( ( Fun 𝑅 ∧ 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑅 finSupp 𝑍 ↔ ( Fun 𝑅 ∧ ( 𝑅 supp 𝑍 ) ∈ Fin ) ) )
3		ibar	⊢ ( Fun 𝑅 → ( ( 𝑅 supp 𝑍 ) ∈ Fin ↔ ( Fun 𝑅 ∧ ( 𝑅 supp 𝑍 ) ∈ Fin ) ) )
4	3	bicomd	⊢ ( Fun 𝑅 → ( ( Fun 𝑅 ∧ ( 𝑅 supp 𝑍 ) ∈ Fin ) ↔ ( 𝑅 supp 𝑍 ) ∈ Fin ) )
5	4	3ad2ant1	⊢ ( ( Fun 𝑅 ∧ 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ( Fun 𝑅 ∧ ( 𝑅 supp 𝑍 ) ∈ Fin ) ↔ ( 𝑅 supp 𝑍 ) ∈ Fin ) )
6	2 5	bitrd	⊢ ( ( Fun 𝑅 ∧ 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑅 finSupp 𝑍 ↔ ( 𝑅 supp 𝑍 ) ∈ Fin ) )