This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )