Proof of Theorem ffsrn
Step | Hyp | Ref
| Expression |
1 | | imaundi 5884 |
. . . . . . 7
⊢ (◡𝐹 “ ((V ∖ {𝑍}) ∪ {𝑍})) = ((◡𝐹 “ (V ∖ {𝑍})) ∪ (◡𝐹 “ {𝑍})) |
2 | 1 | reseq2i 5731 |
. . . . . 6
⊢ (𝐹 ↾ (◡𝐹 “ ((V ∖ {𝑍}) ∪ {𝑍}))) = (𝐹 ↾ ((◡𝐹 “ (V ∖ {𝑍})) ∪ (◡𝐹 “ {𝑍}))) |
3 | | undif1 4338 |
. . . . . . . . 9
⊢ ((V
∖ {𝑍}) ∪ {𝑍}) = (V ∪ {𝑍}) |
4 | | ssv 3912 |
. . . . . . . . . 10
⊢ {𝑍} ⊆ V |
5 | | ssequn2 4080 |
. . . . . . . . . 10
⊢ ({𝑍} ⊆ V ↔ (V ∪
{𝑍}) = V) |
6 | 4, 5 | mpbi 231 |
. . . . . . . . 9
⊢ (V ∪
{𝑍}) = V |
7 | 3, 6 | eqtri 2819 |
. . . . . . . 8
⊢ ((V
∖ {𝑍}) ∪ {𝑍}) = V |
8 | 7 | imaeq2i 5804 |
. . . . . . 7
⊢ (◡𝐹 “ ((V ∖ {𝑍}) ∪ {𝑍})) = (◡𝐹 “ V) |
9 | 8 | reseq2i 5731 |
. . . . . 6
⊢ (𝐹 ↾ (◡𝐹 “ ((V ∖ {𝑍}) ∪ {𝑍}))) = (𝐹 ↾ (◡𝐹 “ V)) |
10 | | resundi 5748 |
. . . . . 6
⊢ (𝐹 ↾ ((◡𝐹 “ (V ∖ {𝑍})) ∪ (◡𝐹 “ {𝑍}))) = ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ (𝐹 ↾ (◡𝐹 “ {𝑍}))) |
11 | 2, 9, 10 | 3eqtr3i 2827 |
. . . . 5
⊢ (𝐹 ↾ (◡𝐹 “ V)) = ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ (𝐹 ↾ (◡𝐹 “ {𝑍}))) |
12 | | ffsrn.1 |
. . . . . 6
⊢ (𝜑 → Fun 𝐹) |
13 | | dfdm4 5650 |
. . . . . . 7
⊢ dom 𝐹 = ran ◡𝐹 |
14 | | dfrn4 5934 |
. . . . . . 7
⊢ ran ◡𝐹 = (◡𝐹 “ V) |
15 | 13, 14 | eqtri 2819 |
. . . . . 6
⊢ dom 𝐹 = (◡𝐹 “ V) |
16 | | df-fn 6228 |
. . . . . . 7
⊢ (𝐹 Fn (◡𝐹 “ V) ↔ (Fun 𝐹 ∧ dom 𝐹 = (◡𝐹 “ V))) |
17 | | fnresdm 6336 |
. . . . . . 7
⊢ (𝐹 Fn (◡𝐹 “ V) → (𝐹 ↾ (◡𝐹 “ V)) = 𝐹) |
18 | 16, 17 | sylbir 236 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ dom 𝐹 = (◡𝐹 “ V)) → (𝐹 ↾ (◡𝐹 “ V)) = 𝐹) |
19 | 12, 15, 18 | sylancl 586 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ (◡𝐹 “ V)) = 𝐹) |
20 | 11, 19 | syl5reqr 2846 |
. . . 4
⊢ (𝜑 → 𝐹 = ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ (𝐹 ↾ (◡𝐹 “ {𝑍})))) |
21 | 20 | rneqd 5690 |
. . 3
⊢ (𝜑 → ran 𝐹 = ran ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ (𝐹 ↾ (◡𝐹 “ {𝑍})))) |
22 | | rnun 5880 |
. . 3
⊢ ran
((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ (𝐹 ↾ (◡𝐹 “ {𝑍}))) = (ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ ran (𝐹 ↾ (◡𝐹 “ {𝑍}))) |
23 | 21, 22 | syl6eq 2847 |
. 2
⊢ (𝜑 → ran 𝐹 = (ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ ran (𝐹 ↾ (◡𝐹 “ {𝑍})))) |
24 | | ffsrn.0 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ 𝑉) |
25 | | ffsrn.z |
. . . . . 6
⊢ (𝜑 → 𝑍 ∈ 𝑊) |
26 | | suppimacnv 7692 |
. . . . . 6
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 supp 𝑍) = (◡𝐹 “ (V ∖ {𝑍}))) |
27 | 24, 25, 26 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝐹 supp 𝑍) = (◡𝐹 “ (V ∖ {𝑍}))) |
28 | | ffsrn.2 |
. . . . 5
⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin) |
29 | 27, 28 | eqeltrrd 2884 |
. . . 4
⊢ (𝜑 → (◡𝐹 “ (V ∖ {𝑍})) ∈ Fin) |
30 | | cnvexg 7485 |
. . . . . 6
⊢ (𝐹 ∈ 𝑉 → ◡𝐹 ∈ V) |
31 | | imaexg 7476 |
. . . . . 6
⊢ (◡𝐹 ∈ V → (◡𝐹 “ (V ∖ {𝑍})) ∈ V) |
32 | 24, 30, 31 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (◡𝐹 “ (V ∖ {𝑍})) ∈ V) |
33 | | cnvimass 5825 |
. . . . . . 7
⊢ (◡𝐹 “ (V ∖ {𝑍})) ⊆ dom 𝐹 |
34 | | fores 6468 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ (◡𝐹 “ (V ∖ {𝑍})) ⊆ dom 𝐹) → (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))):(◡𝐹 “ (V ∖ {𝑍}))–onto→(𝐹 “ (◡𝐹 “ (V ∖ {𝑍})))) |
35 | 12, 33, 34 | sylancl 586 |
. . . . . 6
⊢ (𝜑 → (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))):(◡𝐹 “ (V ∖ {𝑍}))–onto→(𝐹 “ (◡𝐹 “ (V ∖ {𝑍})))) |
36 | | fofn 6460 |
. . . . . 6
⊢ ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))):(◡𝐹 “ (V ∖ {𝑍}))–onto→(𝐹 “ (◡𝐹 “ (V ∖ {𝑍}))) → (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) Fn (◡𝐹 “ (V ∖ {𝑍}))) |
37 | 35, 36 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) Fn (◡𝐹 “ (V ∖ {𝑍}))) |
38 | | fnrndomg 9804 |
. . . . 5
⊢ ((◡𝐹 “ (V ∖ {𝑍})) ∈ V → ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) Fn (◡𝐹 “ (V ∖ {𝑍})) → ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ≼ (◡𝐹 “ (V ∖ {𝑍})))) |
39 | 32, 37, 38 | sylc 65 |
. . . 4
⊢ (𝜑 → ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ≼ (◡𝐹 “ (V ∖ {𝑍}))) |
40 | | domfi 8585 |
. . . 4
⊢ (((◡𝐹 “ (V ∖ {𝑍})) ∈ Fin ∧ ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ≼ (◡𝐹 “ (V ∖ {𝑍}))) → ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∈ Fin) |
41 | 29, 39, 40 | syl2anc 584 |
. . 3
⊢ (𝜑 → ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∈ Fin) |
42 | | snfi 8442 |
. . . 4
⊢ {𝑍} ∈ Fin |
43 | | df-ima 5456 |
. . . . . 6
⊢ (𝐹 “ (◡𝐹 “ {𝑍})) = ran (𝐹 ↾ (◡𝐹 “ {𝑍})) |
44 | | funimacnv 6305 |
. . . . . . 7
⊢ (Fun
𝐹 → (𝐹 “ (◡𝐹 “ {𝑍})) = ({𝑍} ∩ ran 𝐹)) |
45 | 12, 44 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐹 “ (◡𝐹 “ {𝑍})) = ({𝑍} ∩ ran 𝐹)) |
46 | 43, 45 | syl5eqr 2845 |
. . . . 5
⊢ (𝜑 → ran (𝐹 ↾ (◡𝐹 “ {𝑍})) = ({𝑍} ∩ ran 𝐹)) |
47 | | inss1 4125 |
. . . . 5
⊢ ({𝑍} ∩ ran 𝐹) ⊆ {𝑍} |
48 | 46, 47 | syl6eqss 3942 |
. . . 4
⊢ (𝜑 → ran (𝐹 ↾ (◡𝐹 “ {𝑍})) ⊆ {𝑍}) |
49 | | ssfi 8584 |
. . . 4
⊢ (({𝑍} ∈ Fin ∧ ran (𝐹 ↾ (◡𝐹 “ {𝑍})) ⊆ {𝑍}) → ran (𝐹 ↾ (◡𝐹 “ {𝑍})) ∈ Fin) |
50 | 42, 48, 49 | sylancr 587 |
. . 3
⊢ (𝜑 → ran (𝐹 ↾ (◡𝐹 “ {𝑍})) ∈ Fin) |
51 | | unfi 8631 |
. . 3
⊢ ((ran
(𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∈ Fin ∧ ran (𝐹 ↾ (◡𝐹 “ {𝑍})) ∈ Fin) → (ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ ran (𝐹 ↾ (◡𝐹 “ {𝑍}))) ∈ Fin) |
52 | 41, 50, 51 | syl2anc 584 |
. 2
⊢ (𝜑 → (ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ ran (𝐹 ↾ (◡𝐹 “ {𝑍}))) ∈ Fin) |
53 | 23, 52 | eqeltrd 2883 |
1
⊢ (𝜑 → ran 𝐹 ∈ Fin) |