Proof of Theorem fsupprnfi
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | snfi 9083 | . 2
⊢ { 0 } ∈
Fin | 
| 2 |  | simpll 767 | . . . 4
⊢ (((Fun
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → Fun 𝐹) | 
| 3 |  | simplr 769 | . . . 4
⊢ (((Fun
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → 𝐹 ∈ 𝑉) | 
| 4 |  | simprl 771 | . . . 4
⊢ (((Fun
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → 0 ∈ 𝑊) | 
| 5 |  | ressupprn 32699 | . . . 4
⊢ ((Fun
𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊) → ran (𝐹 ↾ (𝐹 supp 0 )) = (ran 𝐹 ∖ { 0 })) | 
| 6 | 2, 3, 4, 5 | syl3anc 1373 | . . 3
⊢ (((Fun
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → ran (𝐹 ↾ (𝐹 supp 0 )) = (ran 𝐹 ∖ { 0 })) | 
| 7 |  | simprr 773 | . . . . 5
⊢ (((Fun
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → 𝐹 finSupp 0 ) | 
| 8 | 7 | fsuppimpd 9409 | . . . 4
⊢ (((Fun
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → (𝐹 supp 0 ) ∈
Fin) | 
| 9 |  | suppssdm 8202 | . . . . . 6
⊢ (𝐹 supp 0 ) ⊆ dom 𝐹 | 
| 10 |  | ssdmres 6031 | . . . . . 6
⊢ ((𝐹 supp 0 ) ⊆ dom 𝐹 ↔ dom (𝐹 ↾ (𝐹 supp 0 )) = (𝐹 supp 0 )) | 
| 11 | 9, 10 | mpbi 230 | . . . . 5
⊢ dom
(𝐹 ↾ (𝐹 supp 0 )) = (𝐹 supp 0 ) | 
| 12 | 2 | funresd 6609 | . . . . . 6
⊢ (((Fun
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → Fun (𝐹 ↾ (𝐹 supp 0 ))) | 
| 13 |  | funforn 6827 | . . . . . 6
⊢ (Fun
(𝐹 ↾ (𝐹 supp 0 )) ↔ (𝐹 ↾ (𝐹 supp 0 )):dom (𝐹 ↾ (𝐹 supp 0 ))–onto→ran (𝐹 ↾ (𝐹 supp 0 ))) | 
| 14 | 12, 13 | sylib 218 | . . . . 5
⊢ (((Fun
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → (𝐹 ↾ (𝐹 supp 0 )):dom (𝐹 ↾ (𝐹 supp 0 ))–onto→ran (𝐹 ↾ (𝐹 supp 0 ))) | 
| 15 |  | foeq2 6817 | . . . . . 6
⊢ (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 476 | . . . . 5
⊢ ((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 587 | . . . 4
⊢ (((Fun
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → (𝐹 ↾ (𝐹 supp 0 )):(𝐹 supp 0 )–onto→ran (𝐹 ↾ (𝐹 supp 0 ))) | 
| 18 |  | fofi 9351 | . . . 4
⊢ (((𝐹 supp 0 ) ∈ Fin ∧ (𝐹 ↾ (𝐹 supp 0 )):(𝐹 supp 0 )–onto→ran (𝐹 ↾ (𝐹 supp 0 ))) → ran (𝐹 ↾ (𝐹 supp 0 )) ∈
Fin) | 
| 19 | 8, 17, 18 | syl2anc 584 | . . 3
⊢ (((Fun
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → ran (𝐹 ↾ (𝐹 supp 0 )) ∈
Fin) | 
| 20 | 6, 19 | eqeltrrd 2842 | . 2
⊢ (((Fun
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → (ran 𝐹 ∖ { 0 }) ∈
Fin) | 
| 21 |  | diffib 32540 | . . 3
⊢ ({ 0 } ∈ Fin
→ (ran 𝐹 ∈ Fin
↔ (ran 𝐹 ∖ {
0 })
∈ Fin)) | 
| 22 | 21 | biimpar 477 | . 2
⊢ (({ 0 } ∈ Fin
∧ (ran 𝐹 ∖ {
0 })
∈ Fin) → ran 𝐹
∈ Fin) | 
| 23 | 1, 20, 22 | sylancr 587 | 1
⊢ (((Fun
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → ran 𝐹 ∈ Fin) |