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 ) = ( ◡ 𝐹 “ ℕ ) ) |
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 ) = ( ◡ 𝐹 “ ℕ ) ) |