Step |
Hyp |
Ref |
Expression |
1 |
|
c0ex |
⊢ 0 ∈ V |
2 |
|
frnfsuppbi |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 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 ) ) |