Proof of Theorem fsupprnfi
Step | Hyp | Ref
| Expression |
1 | | snfi 8607 |
. 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 30533 |
. . . 4
⊢ ((Fun
𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊) → ran (𝐹 ↾ (𝐹 supp 0 )) = (ran 𝐹 ∖ { 0 })) |
6 | 2, 3, 4, 5 | syl3anc 1369 |
. . 3
⊢ (((Fun
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → ran (𝐹 ↾ (𝐹 supp 0 )) = (ran 𝐹 ∖ { 0 })) |
7 | | simprr 773 |
. . . . 5
⊢ (((Fun
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → 𝐹 finSupp 0 ) |
8 | 7 | fsuppimpd 8858 |
. . . 4
⊢ (((Fun
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → (𝐹 supp 0 ) ∈
Fin) |
9 | | suppssdm 7844 |
. . . . . 6
⊢ (𝐹 supp 0 ) ⊆ dom 𝐹 |
10 | | ssdmres 5839 |
. . . . . 6
⊢ ((𝐹 supp 0 ) ⊆ dom 𝐹 ↔ dom (𝐹 ↾ (𝐹 supp 0 )) = (𝐹 supp 0 )) |
11 | 9, 10 | mpbi 233 |
. . . . 5
⊢ dom
(𝐹 ↾ (𝐹 supp 0 )) = (𝐹 supp 0 ) |
12 | 2 | funresd 6371 |
. . . . . 6
⊢ (((Fun
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → Fun (𝐹 ↾ (𝐹 supp 0 ))) |
13 | | funforn 6576 |
. . . . . 6
⊢ (Fun
(𝐹 ↾ (𝐹 supp 0 )) ↔ (𝐹 ↾ (𝐹 supp 0 )):dom (𝐹 ↾ (𝐹 supp 0 ))–onto→ran (𝐹 ↾ (𝐹 supp 0 ))) |
14 | 12, 13 | sylib 221 |
. . . . 5
⊢ (((Fun
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → (𝐹 ↾ (𝐹 supp 0 )):dom (𝐹 ↾ (𝐹 supp 0 ))–onto→ran (𝐹 ↾ (𝐹 supp 0 ))) |
15 | | foeq2 6566 |
. . . . . 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 481 |
. . . . 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 591 |
. . . 4
⊢ (((Fun
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → (𝐹 ↾ (𝐹 supp 0 )):(𝐹 supp 0 )–onto→ran (𝐹 ↾ (𝐹 supp 0 ))) |
18 | | fofi 8828 |
. . . 4
⊢ (((𝐹 supp 0 ) ∈ Fin ∧ (𝐹 ↾ (𝐹 supp 0 )):(𝐹 supp 0 )–onto→ran (𝐹 ↾ (𝐹 supp 0 ))) → ran (𝐹 ↾ (𝐹 supp 0 )) ∈
Fin) |
19 | 8, 17, 18 | syl2anc 588 |
. . 3
⊢ (((Fun
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → ran (𝐹 ↾ (𝐹 supp 0 )) ∈
Fin) |
20 | 6, 19 | eqeltrrd 2852 |
. 2
⊢ (((Fun
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → (ran 𝐹 ∖ { 0 }) ∈
Fin) |
21 | | diffib 30376 |
. . 3
⊢ ({ 0 } ∈ Fin
→ (ran 𝐹 ∈ Fin
↔ (ran 𝐹 ∖ {
0 })
∈ Fin)) |
22 | 21 | biimpar 482 |
. 2
⊢ (({ 0 } ∈ Fin
∧ (ran 𝐹 ∖ {
0 })
∈ Fin) → ran 𝐹
∈ Fin) |
23 | 1, 20, 22 | sylancr 591 |
1
⊢ (((Fun
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → ran 𝐹 ∈ Fin) |