Step |
Hyp |
Ref |
Expression |
1 |
|
fsuppinisegfi.1 |
⊢ ( 𝜑 → 𝐹 ∈ 𝑉 ) |
2 |
|
fsuppinisegfi.2 |
⊢ ( 𝜑 → 0 ∈ 𝑊 ) |
3 |
|
fsuppinisegfi.3 |
⊢ ( 𝜑 → 𝑌 ∈ ( V ∖ { 0 } ) ) |
4 |
|
fsuppinisegfi.4 |
⊢ ( 𝜑 → 𝐹 finSupp 0 ) |
5 |
4
|
fsuppimpd |
⊢ ( 𝜑 → ( 𝐹 supp 0 ) ∈ Fin ) |
6 |
3
|
snssd |
⊢ ( 𝜑 → { 𝑌 } ⊆ ( V ∖ { 0 } ) ) |
7 |
|
imass2 |
⊢ ( { 𝑌 } ⊆ ( V ∖ { 0 } ) → ( ◡ 𝐹 “ { 𝑌 } ) ⊆ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) |
8 |
6 7
|
syl |
⊢ ( 𝜑 → ( ◡ 𝐹 “ { 𝑌 } ) ⊆ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) |
9 |
|
suppimacnvss |
⊢ ( ( 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) → ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ⊆ ( 𝐹 supp 0 ) ) |
10 |
1 2 9
|
syl2anc |
⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ⊆ ( 𝐹 supp 0 ) ) |
11 |
8 10
|
sstrd |
⊢ ( 𝜑 → ( ◡ 𝐹 “ { 𝑌 } ) ⊆ ( 𝐹 supp 0 ) ) |
12 |
5 11
|
ssfid |
⊢ ( 𝜑 → ( ◡ 𝐹 “ { 𝑌 } ) ∈ Fin ) |