Proof of Theorem ffsrn
Step | Hyp | Ref
| Expression |
1 | | imaundi 5464 |
. . . . . . 7
⊢ (◡𝐹 “ ((V ∖ {𝑍}) ∪ {𝑍})) = ((◡𝐹 “ (V ∖ {𝑍})) ∪ (◡𝐹 “ {𝑍})) |
2 | 1 | reseq2i 5314 |
. . . . . 6
⊢ (𝐹 ↾ (◡𝐹 “ ((V ∖ {𝑍}) ∪ {𝑍}))) = (𝐹 ↾ ((◡𝐹 “ (V ∖ {𝑍})) ∪ (◡𝐹 “ {𝑍}))) |
3 | | undif1 3995 |
. . . . . . . . 9
⊢ ((V
∖ {𝑍}) ∪ {𝑍}) = (V ∪ {𝑍}) |
4 | | ssv 3588 |
. . . . . . . . . 10
⊢ {𝑍} ⊆ V |
5 | | ssequn2 3748 |
. . . . . . . . . 10
⊢ ({𝑍} ⊆ V ↔ (V ∪
{𝑍}) = V) |
6 | 4, 5 | mpbi 219 |
. . . . . . . . 9
⊢ (V ∪
{𝑍}) = V |
7 | 3, 6 | eqtri 2632 |
. . . . . . . 8
⊢ ((V
∖ {𝑍}) ∪ {𝑍}) = V |
8 | 7 | imaeq2i 5383 |
. . . . . . 7
⊢ (◡𝐹 “ ((V ∖ {𝑍}) ∪ {𝑍})) = (◡𝐹 “ V) |
9 | 8 | reseq2i 5314 |
. . . . . 6
⊢ (𝐹 ↾ (◡𝐹 “ ((V ∖ {𝑍}) ∪ {𝑍}))) = (𝐹 ↾ (◡𝐹 “ V)) |
10 | | resundi 5330 |
. . . . . 6
⊢ (𝐹 ↾ ((◡𝐹 “ (V ∖ {𝑍})) ∪ (◡𝐹 “ {𝑍}))) = ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ (𝐹 ↾ (◡𝐹 “ {𝑍}))) |
11 | 2, 9, 10 | 3eqtr3i 2640 |
. . . . 5
⊢ (𝐹 ↾ (◡𝐹 “ V)) = ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ (𝐹 ↾ (◡𝐹 “ {𝑍}))) |
12 | | ffsrn.1 |
. . . . . 6
⊢ (𝜑 → Fun 𝐹) |
13 | | dfdm4 5238 |
. . . . . . 7
⊢ dom 𝐹 = ran ◡𝐹 |
14 | | dfrn4 5513 |
. . . . . . 7
⊢ ran ◡𝐹 = (◡𝐹 “ V) |
15 | 13, 14 | eqtri 2632 |
. . . . . 6
⊢ dom 𝐹 = (◡𝐹 “ V) |
16 | | df-fn 5807 |
. . . . . . 7
⊢ (𝐹 Fn (◡𝐹 “ V) ↔ (Fun 𝐹 ∧ dom 𝐹 = (◡𝐹 “ V))) |
17 | | fnresdm 5914 |
. . . . . . 7
⊢ (𝐹 Fn (◡𝐹 “ V) → (𝐹 ↾ (◡𝐹 “ V)) = 𝐹) |
18 | 16, 17 | sylbir 224 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ dom 𝐹 = (◡𝐹 “ V)) → (𝐹 ↾ (◡𝐹 “ V)) = 𝐹) |
19 | 12, 15, 18 | sylancl 693 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ (◡𝐹 “ V)) = 𝐹) |
20 | 11, 19 | syl5reqr 2659 |
. . . 4
⊢ (𝜑 → 𝐹 = ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ (𝐹 ↾ (◡𝐹 “ {𝑍})))) |
21 | 20 | rneqd 5274 |
. . 3
⊢ (𝜑 → ran 𝐹 = ran ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ (𝐹 ↾ (◡𝐹 “ {𝑍})))) |
22 | | rnun 5460 |
. . 3
⊢ ran
((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ (𝐹 ↾ (◡𝐹 “ {𝑍}))) = (ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ ran (𝐹 ↾ (◡𝐹 “ {𝑍}))) |
23 | 21, 22 | syl6eq 2660 |
. 2
⊢ (𝜑 → ran 𝐹 = (ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ ran (𝐹 ↾ (◡𝐹 “ {𝑍})))) |
24 | | ffsrn.0 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ 𝑉) |
25 | | ffsrn.z |
. . . . . 6
⊢ (𝜑 → 𝑍 ∈ 𝑊) |
26 | | suppimacnv 7193 |
. . . . . 6
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 supp 𝑍) = (◡𝐹 “ (V ∖ {𝑍}))) |
27 | 24, 25, 26 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝐹 supp 𝑍) = (◡𝐹 “ (V ∖ {𝑍}))) |
28 | | ffsrn.2 |
. . . . 5
⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin) |
29 | 27, 28 | eqeltrrd 2689 |
. . . 4
⊢ (𝜑 → (◡𝐹 “ (V ∖ {𝑍})) ∈ Fin) |
30 | | cnvexg 7005 |
. . . . . 6
⊢ (𝐹 ∈ 𝑉 → ◡𝐹 ∈ V) |
31 | | imaexg 6995 |
. . . . . 6
⊢ (◡𝐹 ∈ V → (◡𝐹 “ (V ∖ {𝑍})) ∈ V) |
32 | 24, 30, 31 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (◡𝐹 “ (V ∖ {𝑍})) ∈ V) |
33 | | cnvimass 5404 |
. . . . . . 7
⊢ (◡𝐹 “ (V ∖ {𝑍})) ⊆ dom 𝐹 |
34 | | fores 6037 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ (◡𝐹 “ (V ∖ {𝑍})) ⊆ dom 𝐹) → (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))):(◡𝐹 “ (V ∖ {𝑍}))–onto→(𝐹 “ (◡𝐹 “ (V ∖ {𝑍})))) |
35 | 12, 33, 34 | sylancl 693 |
. . . . . 6
⊢ (𝜑 → (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))):(◡𝐹 “ (V ∖ {𝑍}))–onto→(𝐹 “ (◡𝐹 “ (V ∖ {𝑍})))) |
36 | | fofn 6030 |
. . . . . 6
⊢ ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))):(◡𝐹 “ (V ∖ {𝑍}))–onto→(𝐹 “ (◡𝐹 “ (V ∖ {𝑍}))) → (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) Fn (◡𝐹 “ (V ∖ {𝑍}))) |
37 | 35, 36 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) Fn (◡𝐹 “ (V ∖ {𝑍}))) |
38 | | fnrndomg 9239 |
. . . . 5
⊢ ((◡𝐹 “ (V ∖ {𝑍})) ∈ V → ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) Fn (◡𝐹 “ (V ∖ {𝑍})) → ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ≼ (◡𝐹 “ (V ∖ {𝑍})))) |
39 | 32, 37, 38 | sylc 63 |
. . . 4
⊢ (𝜑 → ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ≼ (◡𝐹 “ (V ∖ {𝑍}))) |
40 | | domfi 8066 |
. . . 4
⊢ (((◡𝐹 “ (V ∖ {𝑍})) ∈ Fin ∧ ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ≼ (◡𝐹 “ (V ∖ {𝑍}))) → ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∈ Fin) |
41 | 29, 39, 40 | syl2anc 691 |
. . 3
⊢ (𝜑 → ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∈ Fin) |
42 | | snfi 7923 |
. . . 4
⊢ {𝑍} ∈ Fin |
43 | | df-ima 5051 |
. . . . . 6
⊢ (𝐹 “ (◡𝐹 “ {𝑍})) = ran (𝐹 ↾ (◡𝐹 “ {𝑍})) |
44 | | funimacnv 5884 |
. . . . . . 7
⊢ (Fun
𝐹 → (𝐹 “ (◡𝐹 “ {𝑍})) = ({𝑍} ∩ ran 𝐹)) |
45 | 12, 44 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐹 “ (◡𝐹 “ {𝑍})) = ({𝑍} ∩ ran 𝐹)) |
46 | 43, 45 | syl5eqr 2658 |
. . . . 5
⊢ (𝜑 → ran (𝐹 ↾ (◡𝐹 “ {𝑍})) = ({𝑍} ∩ ran 𝐹)) |
47 | | inss1 3795 |
. . . . 5
⊢ ({𝑍} ∩ ran 𝐹) ⊆ {𝑍} |
48 | 46, 47 | syl6eqss 3618 |
. . . 4
⊢ (𝜑 → ran (𝐹 ↾ (◡𝐹 “ {𝑍})) ⊆ {𝑍}) |
49 | | ssfi 8065 |
. . . 4
⊢ (({𝑍} ∈ Fin ∧ ran (𝐹 ↾ (◡𝐹 “ {𝑍})) ⊆ {𝑍}) → ran (𝐹 ↾ (◡𝐹 “ {𝑍})) ∈ Fin) |
50 | 42, 48, 49 | sylancr 694 |
. . 3
⊢ (𝜑 → ran (𝐹 ↾ (◡𝐹 “ {𝑍})) ∈ Fin) |
51 | | unfi 8112 |
. . 3
⊢ ((ran
(𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∈ Fin ∧ ran (𝐹 ↾ (◡𝐹 “ {𝑍})) ∈ Fin) → (ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ ran (𝐹 ↾ (◡𝐹 “ {𝑍}))) ∈ Fin) |
52 | 41, 50, 51 | syl2anc 691 |
. 2
⊢ (𝜑 → (ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ ran (𝐹 ↾ (◡𝐹 “ {𝑍}))) ∈ Fin) |
53 | 23, 52 | eqeltrd 2688 |
1
⊢ (𝜑 → ran 𝐹 ∈ Fin) |