Theorem ffsrn 32659

Description: The range of a finitely supported function is finite. (Contributed by Thierry Arnoux, 27-Aug-2017.)

Hypotheses

Ref	Expression
ffsrn.z	⊢ (𝜑 → 𝑍 ∈ 𝑊)
ffsrn.0	⊢ (𝜑 → 𝐹 ∈ 𝑉)
ffsrn.1	⊢ (𝜑 → Fun 𝐹)
ffsrn.2	⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)

Assertion

Ref	Expression
ffsrn	⊢ (𝜑 → ran 𝐹 ∈ Fin)

Proof of Theorem ffsrn

Step	Hyp	Ref	Expression
1		ffsrn.1	. . . . . 6 ⊢ (𝜑 → Fun 𝐹)
2		dfdm4 5862	. . . . . . 7 ⊢ dom 𝐹 = ran ◡𝐹
3		dfrn4 6178	. . . . . . 7 ⊢ ran ◡𝐹 = (◡𝐹 “ V)
4	2, 3	eqtri 2753	. . . . . 6 ⊢ dom 𝐹 = (◡𝐹 “ V)
5		df-fn 6517	. . . . . . 7 ⊢ (𝐹 Fn (◡𝐹 “ V) ↔ (Fun 𝐹 ∧ dom 𝐹 = (◡𝐹 “ V)))
6		fnresdm 6640	. . . . . . 7 ⊢ (𝐹 Fn (◡𝐹 “ V) → (𝐹 ↾ (◡𝐹 “ V)) = 𝐹)
7	5, 6	sylbir 235	. . . . . 6 ⊢ ((Fun 𝐹 ∧ dom 𝐹 = (◡𝐹 “ V)) → (𝐹 ↾ (◡𝐹 “ V)) = 𝐹)
8	1, 4, 7	sylancl 586	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ (◡𝐹 “ V)) = 𝐹)
9		imaundi 6125	. . . . . . 7 ⊢ (◡𝐹 “ ((V ∖ {𝑍}) ∪ {𝑍})) = ((◡𝐹 “ (V ∖ {𝑍})) ∪ (◡𝐹 “ {𝑍}))
10	9	reseq2i 5950	. . . . . 6 ⊢ (𝐹 ↾ (◡𝐹 “ ((V ∖ {𝑍}) ∪ {𝑍}))) = (𝐹 ↾ ((◡𝐹 “ (V ∖ {𝑍})) ∪ (◡𝐹 “ {𝑍})))
11		undif1 4442	. . . . . . . . 9 ⊢ ((V ∖ {𝑍}) ∪ {𝑍}) = (V ∪ {𝑍})
12		ssv 3974	. . . . . . . . . 10 ⊢ {𝑍} ⊆ V
13		ssequn2 4155	. . . . . . . . . 10 ⊢ ({𝑍} ⊆ V ↔ (V ∪ {𝑍}) = V)
14	12, 13	mpbi 230	. . . . . . . . 9 ⊢ (V ∪ {𝑍}) = V
15	11, 14	eqtri 2753	. . . . . . . 8 ⊢ ((V ∖ {𝑍}) ∪ {𝑍}) = V
16	15	imaeq2i 6032	. . . . . . 7 ⊢ (◡𝐹 “ ((V ∖ {𝑍}) ∪ {𝑍})) = (◡𝐹 “ V)
17	16	reseq2i 5950	. . . . . 6 ⊢ (𝐹 ↾ (◡𝐹 “ ((V ∖ {𝑍}) ∪ {𝑍}))) = (𝐹 ↾ (◡𝐹 “ V))
18		resundi 5967	. . . . . 6 ⊢ (𝐹 ↾ ((◡𝐹 “ (V ∖ {𝑍})) ∪ (◡𝐹 “ {𝑍}))) = ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ (𝐹 ↾ (◡𝐹 “ {𝑍})))
19	10, 17, 18	3eqtr3i 2761	. . . . 5 ⊢ (𝐹 ↾ (◡𝐹 “ V)) = ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ (𝐹 ↾ (◡𝐹 “ {𝑍})))
20	8, 19	eqtr3di 2780	. . . 4 ⊢ (𝜑 → 𝐹 = ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ (𝐹 ↾ (◡𝐹 “ {𝑍}))))
21	20	rneqd 5905	. . 3 ⊢ (𝜑 → ran 𝐹 = ran ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ (𝐹 ↾ (◡𝐹 “ {𝑍}))))
22		rnun 6121	. . 3 ⊢ ran ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ (𝐹 ↾ (◡𝐹 “ {𝑍}))) = (ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ ran (𝐹 ↾ (◡𝐹 “ {𝑍})))
23	21, 22	eqtrdi 2781	. 2 ⊢ (𝜑 → ran 𝐹 = (ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∪ ran (𝐹 ↾ (◡𝐹 “ {𝑍}))))
24		ffsrn.0	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ 𝑉)
25		ffsrn.z	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ 𝑊)
26		suppimacnv 8156	. . . . . 6 ⊢ ((𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 supp 𝑍) = (◡𝐹 “ (V ∖ {𝑍})))
27	24, 25, 26	syl2anc 584	. . . . 5 ⊢ (𝜑 → (𝐹 supp 𝑍) = (◡𝐹 “ (V ∖ {𝑍})))
28		ffsrn.2	. . . . 5 ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)
29	27, 28	eqeltrrd 2830	. . . 4 ⊢ (𝜑 → (◡𝐹 “ (V ∖ {𝑍})) ∈ Fin)
30		cnvexg 7903	. . . . . 6 ⊢ (𝐹 ∈ 𝑉 → ◡𝐹 ∈ V)
31		imaexg 7892	. . . . . 6 ⊢ (◡𝐹 ∈ V → (◡𝐹 “ (V ∖ {𝑍})) ∈ V)
32	24, 30, 31	3syl 18	. . . . 5 ⊢ (𝜑 → (◡𝐹 “ (V ∖ {𝑍})) ∈ V)
33		cnvimass 6056	. . . . . . 7 ⊢ (◡𝐹 “ (V ∖ {𝑍})) ⊆ dom 𝐹
34		fores 6785	. . . . . . 7 ⊢ ((Fun 𝐹 ∧ (◡𝐹 “ (V ∖ {𝑍})) ⊆ dom 𝐹) → (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))):(◡𝐹 “ (V ∖ {𝑍}))–onto→(𝐹 “ (◡𝐹 “ (V ∖ {𝑍}))))
35	1, 33, 34	sylancl 586	. . . . . 6 ⊢ (𝜑 → (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))):(◡𝐹 “ (V ∖ {𝑍}))–onto→(𝐹 “ (◡𝐹 “ (V ∖ {𝑍}))))
36		fofn 6777	. . . . . 6 ⊢ ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))):(◡𝐹 “ (V ∖ {𝑍}))–onto→(𝐹 “ (◡𝐹 “ (V ∖ {𝑍}))) → (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) Fn (◡𝐹 “ (V ∖ {𝑍})))
37	35, 36	syl 17	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) Fn (◡𝐹 “ (V ∖ {𝑍})))
38		fnrndomg 10496	. . . . 5 ⊢ ((◡𝐹 “ (V ∖ {𝑍})) ∈ V → ((𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) Fn (◡𝐹 “ (V ∖ {𝑍})) → ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ≼ (◡𝐹 “ (V ∖ {𝑍}))))
39	32, 37, 38	sylc 65	. . . 4 ⊢ (𝜑 → ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ≼ (◡𝐹 “ (V ∖ {𝑍})))
40		domfi 9159	. . . 4 ⊢ (((◡𝐹 “ (V ∖ {𝑍})) ∈ Fin ∧ ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ≼ (◡𝐹 “ (V ∖ {𝑍}))) → ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∈ Fin)
41	29, 39, 40	syl2anc 584	. . 3 ⊢ (𝜑 → ran (𝐹 ↾ (◡𝐹 “ (V ∖ {𝑍}))) ∈ Fin)
42		snfi 9017	. . . 4 ⊢ {𝑍} ∈ Fin
43		df-ima 5654	. . . . . 6 ⊢ (𝐹 “ (◡𝐹 “ {𝑍})) = ran (𝐹 ↾ (◡𝐹 “ {𝑍}))
44		funimacnv 6600	. . . . . . 7 ⊢ (Fun 𝐹 → (𝐹 “ (◡𝐹 “ {𝑍})) = ({𝑍} ∩ ran 𝐹))
45	1, 44	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐹 “ (◡𝐹 “ {𝑍})) = ({𝑍} ∩ ran 𝐹))
46	43, 45	eqtr3id 2779	. . . . 5 ⊢ (𝜑 → ran (𝐹 ↾ (◡𝐹 “ {𝑍})) = ({𝑍} ∩ ran 𝐹))
47		inss1 4203	. . . . 5 ⊢ ({𝑍} ∩ ran 𝐹) ⊆ {𝑍}
48	46, 47	eqsstrdi 3994	. . . 4 ⊢ (𝜑 → ran (𝐹 ↾ (◡𝐹 “ {𝑍})) ⊆ {𝑍})
49		ssfi 9143	. . . 4 ⊢ (({𝑍} ∈ Fin ∧ ran (𝐹 ↾ (◡𝐹 “ {𝑍})) ⊆ {𝑍}) → ran (𝐹 ↾ (◡𝐹 “ {𝑍})) ∈ Fin)
50	42, 48, 49	sylancr 587	. . 3 ⊢ (𝜑 → ran (𝐹 ↾ (◡𝐹 “ {𝑍})) ∈ Fin)
51		unfi 9141	. . 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 2829	1 ⊢ (𝜑 → ran 𝐹 ∈ Fin)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3450   ∖ cdif 3914   ∪ cun 3915   ∩ cin 3916   ⊆ wss 3917  {csn 4592   class class class wbr 5110  ^◡ccnv 5640  dom cdm 5641  ran crn 5642   ↾ cres 5643   “ cima 5644  Fun wfun 6508   Fn wfn 6509  –onto→wfo 6512  (class class class)co 7390   supp csupp 8142   ≼ cdom 8919  Fincfn 8921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-ac2 10423

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-se 5595  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-isom 6523  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7846  df-1st 7971  df-2nd 7972  df-supp 8143  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-1o 8437  df-er 8674  df-map 8804  df-en 8922  df-dom 8923  df-fin 8925  df-card 9899  df-acn 9902  df-ac 10076

This theorem is referenced by:  fpwrelmapffslem  32662