Theorem fcdmnn0fsupp

Description: A function into NN0 is finitely supported iff its support is finite. (Contributed by AV, 8-Jul-2019)

	Ref	Expression
Assertion	fcdmnn0fsupp	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 finSupp 0 ↔ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		c0ex	⊢ 0 ∈ V
2		ffsuppbi	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 0 ∈ V ) → ( 𝐹 : 𝐼 ⟶ ℕ0 → ( 𝐹 finSupp 0 ↔ ( ◡ 𝐹 “ ( ℕ0 ∖ { 0 } ) ) ∈ Fin ) ) )
3	1 2	mpan2	⊢ ( 𝐼 ∈ 𝑉 → ( 𝐹 : 𝐼 ⟶ ℕ0 → ( 𝐹 finSupp 0 ↔ ( ◡ 𝐹 “ ( ℕ0 ∖ { 0 } ) ) ∈ Fin ) ) )
4	3	imp	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 finSupp 0 ↔ ( ◡ 𝐹 “ ( ℕ0 ∖ { 0 } ) ) ∈ Fin ) )
5		dfn2	⊢ ℕ = ( ℕ0 ∖ { 0 } )
6	5	imaeq2i	⊢ ( ◡ 𝐹 “ ℕ ) = ( ◡ 𝐹 “ ( ℕ0 ∖ { 0 } ) )
7	6	eleq1i	⊢ ( ( ◡ 𝐹 “ ℕ ) ∈ Fin ↔ ( ◡ 𝐹 “ ( ℕ0 ∖ { 0 } ) ) ∈ Fin )
8	4 7	bitr4di	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 finSupp 0 ↔ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) )