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	2	imp	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 0 ∈ V ) ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ( ℕ0 ∖ { 0 } ) ) )
4	1 3	mpanl2	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ( ℕ0 ∖ { 0 } ) ) )
5		dfn2	⊢ ℕ = ( ℕ0 ∖ { 0 } )
6	5	eqcomi	⊢ ( ℕ0 ∖ { 0 } ) = ℕ
7	6	imaeq2i	⊢ ( ◡ 𝐹 “ ( ℕ0 ∖ { 0 } ) ) = ( ◡ 𝐹 “ ℕ )
8	4 7	syl6eq	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ℕ ) )