Step |
Hyp |
Ref |
Expression |
1 |
|
snfi |
⊢ { 0 } ∈ Fin |
2 |
|
simpll |
⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → Fun 𝐹 ) |
3 |
|
simplr |
⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → 𝐹 ∈ 𝑉 ) |
4 |
|
simprl |
⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → 0 ∈ 𝑊 ) |
5 |
|
ressupprn |
⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) → ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( ran 𝐹 ∖ { 0 } ) ) |
6 |
2 3 4 5
|
syl3anc |
⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( ran 𝐹 ∖ { 0 } ) ) |
7 |
|
simprr |
⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → 𝐹 finSupp 0 ) |
8 |
7
|
fsuppimpd |
⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → ( 𝐹 supp 0 ) ∈ Fin ) |
9 |
|
suppssdm |
⊢ ( 𝐹 supp 0 ) ⊆ dom 𝐹 |
10 |
|
ssdmres |
⊢ ( ( 𝐹 supp 0 ) ⊆ dom 𝐹 ↔ dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝐹 supp 0 ) ) |
11 |
9 10
|
mpbi |
⊢ dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝐹 supp 0 ) |
12 |
2
|
funresd |
⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → Fun ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) |
13 |
|
funforn |
⊢ ( Fun ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↔ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) : dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) –onto→ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) |
14 |
12 13
|
sylib |
⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) : dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) –onto→ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) |
15 |
|
foeq2 |
⊢ ( dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝐹 supp 0 ) → ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) : dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) –onto→ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↔ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) : ( 𝐹 supp 0 ) –onto→ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) ) |
16 |
15
|
biimpa |
⊢ ( ( dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝐹 supp 0 ) ∧ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) : dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) –onto→ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) : ( 𝐹 supp 0 ) –onto→ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) |
17 |
11 14 16
|
sylancr |
⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) : ( 𝐹 supp 0 ) –onto→ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) |
18 |
|
fofi |
⊢ ( ( ( 𝐹 supp 0 ) ∈ Fin ∧ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) : ( 𝐹 supp 0 ) –onto→ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∈ Fin ) |
19 |
8 17 18
|
syl2anc |
⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∈ Fin ) |
20 |
6 19
|
eqeltrrd |
⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → ( ran 𝐹 ∖ { 0 } ) ∈ Fin ) |
21 |
|
diffib |
⊢ ( { 0 } ∈ Fin → ( ran 𝐹 ∈ Fin ↔ ( ran 𝐹 ∖ { 0 } ) ∈ Fin ) ) |
22 |
21
|
biimpar |
⊢ ( ( { 0 } ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ∈ Fin ) → ran 𝐹 ∈ Fin ) |
23 |
1 20 22
|
sylancr |
⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → ran 𝐹 ∈ Fin ) |