Proof of Theorem ffsrn
Step | Hyp | Ref
| Expression |
1 | | ffsrn.1 |
. . . . . 6
⊢ (𝜑 → Fun 𝐹) |
2 | | dfdm4 5804 |
. . . . . . 7
⊢ dom 𝐹 = ran ◡𝐹 |
3 | | dfrn4 6105 |
. . . . . . 7
⊢ ran ◡𝐹 = (◡𝐹 “ V) |
4 | 2, 3 | eqtri 2766 |
. . . . . 6
⊢ dom 𝐹 = (◡𝐹 “ V) |
5 | | df-fn 6436 |
. . . . . . 7
⊢ (𝐹 Fn (◡𝐹 “ V) ↔ (Fun 𝐹 ∧ dom 𝐹 = (◡𝐹 “ V))) |
6 | | fnresdm 6551 |
. . . . . . 7
⊢ (𝐹 Fn (◡𝐹 “ V) → (𝐹 ↾ (◡𝐹 “ V)) = 𝐹) |
7 | 5, 6 | sylbir 234 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ dom 𝐹 = (◡𝐹 “ V)) → (𝐹 ↾ (◡𝐹 “ V)) = 𝐹) |
8 | 1, 4, 7 | sylancl 586 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ (◡𝐹 “ V)) = 𝐹) |
9 | | imaundi 6053 |
. . . . . . 7
⊢ (◡𝐹 “ ((V ∖ {𝑍}) ∪ {𝑍})) = ((◡𝐹 “ (V ∖ {𝑍})) ∪ (◡𝐹 “ {𝑍})) |
10 | 9 | reseq2i 5888 |
. . . . . 6
⊢ (𝐹 ↾ (◡𝐹 “ ((V ∖ {𝑍}) ∪ {𝑍}))) = (𝐹 ↾ ((◡𝐹 “ (V ∖ {𝑍})) ∪ (◡𝐹 “ {𝑍}))) |
11 | | undif1 4409 |
. . . . . . . . 9
⊢ ((V
∖ {𝑍}) ∪ {𝑍}) = (V ∪ {𝑍}) |
12 | | ssv 3945 |
. . . . . . . . . 10
⊢ {𝑍} ⊆ V |
13 | | ssequn2 4117 |
. . . . . . . . . 10
⊢ ({𝑍} ⊆ V ↔ (V ∪
{𝑍}) = V) |
14 | 12, 13 | mpbi 229 |
. . . . . . . . 9
⊢ (V ∪
{𝑍}) = V |
15 | 11, 14 | eqtri 2766 |
. . . . . . . 8
⊢ ((V
∖ {𝑍}) ∪ {𝑍}) = V |
16 | 15 | imaeq2i 5967 |
. . . . . . 7
⊢ (◡𝐹 “ ((V ∖ {𝑍}) ∪ {𝑍})) = (◡𝐹 “ V) |
17 | 16 | reseq2i 5888 |
. . . . . 6
⊢ (𝐹 ↾ (◡𝐹 “ ((V ∖ {𝑍}) ∪ {𝑍}))) = (𝐹 ↾ (◡𝐹 “ V)) |
18 | | resundi 5905 |
. . . . . 6
⊢ (𝐹 ↾ ((◡𝐹 “ (V ∖ {𝑍})) ∪ (◡𝐹 “ {𝑍}))) = ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ (𝐹 ↾ (◡𝐹 “ {𝑍}))) |
19 | 10, 17, 18 | 3eqtr3i 2774 |
. . . . 5
⊢ (𝐹 ↾ (◡𝐹 “ V)) = ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ (𝐹 ↾ (◡𝐹 “ {𝑍}))) |
20 | 8, 19 | eqtr3di 2793 |
. . . 4
⊢ (𝜑 → 𝐹 = ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ (𝐹 ↾ (◡𝐹 “ {𝑍})))) |
21 | 20 | rneqd 5847 |
. . 3
⊢ (𝜑 → ran 𝐹 = ran ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ (𝐹 ↾ (◡𝐹 “ {𝑍})))) |
22 | | rnun 6049 |
. . 3
⊢ ran
((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ (𝐹 ↾ (◡𝐹 “ {𝑍}))) = (ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ ran (𝐹 ↾ (◡𝐹 “ {𝑍}))) |
23 | 21, 22 | eqtrdi 2794 |
. 2
⊢ (𝜑 → ran 𝐹 = (ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ ran (𝐹 ↾ (◡𝐹 “ {𝑍})))) |
24 | | ffsrn.0 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ 𝑉) |
25 | | ffsrn.z |
. . . . . 6
⊢ (𝜑 → 𝑍 ∈ 𝑊) |
26 | | suppimacnv 7990 |
. . . . . 6
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 supp 𝑍) = (◡𝐹 “ (V ∖ {𝑍}))) |
27 | 24, 25, 26 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝐹 supp 𝑍) = (◡𝐹 “ (V ∖ {𝑍}))) |
28 | | ffsrn.2 |
. . . . 5
⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin) |
29 | 27, 28 | eqeltrrd 2840 |
. . . 4
⊢ (𝜑 → (◡𝐹 “ (V ∖ {𝑍})) ∈ Fin) |
30 | | cnvexg 7771 |
. . . . . 6
⊢ (𝐹 ∈ 𝑉 → ◡𝐹 ∈ V) |
31 | | imaexg 7762 |
. . . . . 6
⊢ (◡𝐹 ∈ V → (◡𝐹 “ (V ∖ {𝑍})) ∈ V) |
32 | 24, 30, 31 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (◡𝐹 “ (V ∖ {𝑍})) ∈ V) |
33 | | cnvimass 5989 |
. . . . . . 7
⊢ (◡𝐹 “ (V ∖ {𝑍})) ⊆ dom 𝐹 |
34 | | fores 6698 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ (◡𝐹 “ (V ∖ {𝑍})) ⊆ dom 𝐹) → (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))):(◡𝐹 “ (V ∖ {𝑍}))–onto→(𝐹 “ (◡𝐹 “ (V ∖ {𝑍})))) |
35 | 1, 33, 34 | sylancl 586 |
. . . . . 6
⊢ (𝜑 → (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))):(◡𝐹 “ (V ∖ {𝑍}))–onto→(𝐹 “ (◡𝐹 “ (V ∖ {𝑍})))) |
36 | | fofn 6690 |
. . . . . 6
⊢ ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))):(◡𝐹 “ (V ∖ {𝑍}))–onto→(𝐹 “ (◡𝐹 “ (V ∖ {𝑍}))) → (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) Fn (◡𝐹 “ (V ∖ {𝑍}))) |
37 | 35, 36 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) Fn (◡𝐹 “ (V ∖ {𝑍}))) |
38 | | fnrndomg 10292 |
. . . . 5
⊢ ((◡𝐹 “ (V ∖ {𝑍})) ∈ V → ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) Fn (◡𝐹 “ (V ∖ {𝑍})) → ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ≼ (◡𝐹 “ (V ∖ {𝑍})))) |
39 | 32, 37, 38 | sylc 65 |
. . . 4
⊢ (𝜑 → ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ≼ (◡𝐹 “ (V ∖ {𝑍}))) |
40 | | domfi 8975 |
. . . 4
⊢ (((◡𝐹 “ (V ∖ {𝑍})) ∈ Fin ∧ ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ≼ (◡𝐹 “ (V ∖ {𝑍}))) → ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∈ Fin) |
41 | 29, 39, 40 | syl2anc 584 |
. . 3
⊢ (𝜑 → ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∈ Fin) |
42 | | snfi 8834 |
. . . 4
⊢ {𝑍} ∈ Fin |
43 | | df-ima 5602 |
. . . . . 6
⊢ (𝐹 “ (◡𝐹 “ {𝑍})) = ran (𝐹 ↾ (◡𝐹 “ {𝑍})) |
44 | | funimacnv 6515 |
. . . . . . 7
⊢ (Fun
𝐹 → (𝐹 “ (◡𝐹 “ {𝑍})) = ({𝑍} ∩ ran 𝐹)) |
45 | 1, 44 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐹 “ (◡𝐹 “ {𝑍})) = ({𝑍} ∩ ran 𝐹)) |
46 | 43, 45 | eqtr3id 2792 |
. . . . 5
⊢ (𝜑 → ran (𝐹 ↾ (◡𝐹 “ {𝑍})) = ({𝑍} ∩ ran 𝐹)) |
47 | | inss1 4162 |
. . . . 5
⊢ ({𝑍} ∩ ran 𝐹) ⊆ {𝑍} |
48 | 46, 47 | eqsstrdi 3975 |
. . . 4
⊢ (𝜑 → ran (𝐹 ↾ (◡𝐹 “ {𝑍})) ⊆ {𝑍}) |
49 | | ssfi 8956 |
. . . 4
⊢ (({𝑍} ∈ Fin ∧ ran (𝐹 ↾ (◡𝐹 “ {𝑍})) ⊆ {𝑍}) → ran (𝐹 ↾ (◡𝐹 “ {𝑍})) ∈ Fin) |
50 | 42, 48, 49 | sylancr 587 |
. . 3
⊢ (𝜑 → ran (𝐹 ↾ (◡𝐹 “ {𝑍})) ∈ Fin) |
51 | | unfi 8955 |
. . 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 2839 |
1
⊢ (𝜑 → ran 𝐹 ∈ Fin) |