Metamath Proof Explorer


Theorem frnnn0supp

Description: Two ways to write the support of a function on NN0 . (Contributed by Mario Carneiro, 29-Dec-2014) (Revised by AV, 7-Jul-2019)

Ref Expression
Assertion frnnn0supp ( ( 𝐼𝑉𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 supp 0 ) = ( 𝐹 “ ℕ ) )

Proof

Step Hyp Ref Expression
1 c0ex 0 ∈ V
2 frnsuppeq ( ( 𝐼𝑉 ∧ 0 ∈ V ) → ( 𝐹 : 𝐼 ⟶ ℕ0 → ( 𝐹 supp 0 ) = ( 𝐹 “ ( ℕ0 ∖ { 0 } ) ) ) )
3 1 2 mpan2 ( 𝐼𝑉 → ( 𝐹 : 𝐼 ⟶ ℕ0 → ( 𝐹 supp 0 ) = ( 𝐹 “ ( ℕ0 ∖ { 0 } ) ) ) )
4 3 imp ( ( 𝐼𝑉𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 supp 0 ) = ( 𝐹 “ ( ℕ0 ∖ { 0 } ) ) )
5 dfn2 ℕ = ( ℕ0 ∖ { 0 } )
6 5 imaeq2i ( 𝐹 “ ℕ ) = ( 𝐹 “ ( ℕ0 ∖ { 0 } ) )
7 4 6 eqtr4di ( ( 𝐼𝑉𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 supp 0 ) = ( 𝐹 “ ℕ ) )