Theorem fsuppmapnn0fiubex 12197

Description: If all functions of a finite set of functions over the nonnegative integers are finitely supported, then the support of all these functions is contained in a finite set of sequential integers starting at 0. (Contributed by AV, 2-Oct-2019.)

Assertion

Ref	Expression
fsuppmapnn0fiubex	|- ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) -> ( A. f e. M f finSupp Z -> E. m e. NN0 A. f e. M ( f supp Z ) C_ ( 0 ... m ) ) )

Distinct variable groups:   f, M, m   R, f, m   f, V, m   f, Z, m

Proof of Theorem fsuppmapnn0fiubex

Dummy variable g is distinct from all other variables.

Step	Hyp	Ref	Expression
1		0nn0 10880	. . . . 5 |- 0 e. NN0
2	1	a1i 11	. . . 4 |- ( ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) -> 0 e. NN0 )
3		oveq2 6305	. . . . . . 7 |- ( m = 0 -> ( 0 ... m ) = ( 0 ... 0 ) )
4	3	sseq2d 3489	. . . . . 6 |- ( m = 0 -> ( ( f supp Z ) C_ ( 0 ... m ) <-> ( f supp Z ) C_ ( 0 ... 0 ) ) )
5	4	ralbidv 2862	. . . . 5 |- ( m = 0 -> ( A. f e. M ( f supp Z ) C_ ( 0 ... m ) <-> A. f e. M ( f supp Z ) C_ ( 0 ... 0 ) ) )
6	5	adantl 467	. . . 4 |- ( ( ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) /\ m = 0 ) -> ( A. f e. M ( f supp Z ) C_ ( 0 ... m ) <-> A. f e. M ( f supp Z ) C_ ( 0 ... 0 ) ) )
7		ral0 3899	. . . . . 6 |- A. f e. (/) ( f supp Z ) C_ ( 0 ... 0 )
8		raleq 3023	. . . . . 6 |- ( (/) = M -> ( A. f e. (/) ( f supp Z ) C_ ( 0 ... 0 ) <-> A. f e. M ( f supp Z ) C_ ( 0 ... 0 ) ) )
9	7, 8	mpbii 214	. . . . 5 |- ( (/) = M -> A. f e. M ( f supp Z ) C_ ( 0 ... 0 ) )
10		0ss 3788	. . . . . . 7 |- (/) C_ ( 0 ... 0 )
11		sseq1 3482	. . . . . . 7 |- ( ( f supp Z ) = (/) -> ( ( f supp Z ) C_ ( 0 ... 0 ) <-> (/) C_ ( 0 ... 0 ) ) )
12	10, 11	mpbiri 236	. . . . . 6 |- ( ( f supp Z ) = (/) -> ( f supp Z ) C_ ( 0 ... 0 ) )
13	12	ralimi 2816	. . . . 5 |- ( A. f e. M ( f supp Z ) = (/) -> A. f e. M ( f supp Z ) C_ ( 0 ... 0 ) )
14	9, 13	jaoi 380	. . . 4 |- ( ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) -> A. f e. M ( f supp Z ) C_ ( 0 ... 0 ) )
15	2, 6, 14	rspcedvd 3184	. . 3 |- ( ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) -> E. m e. NN0 A. f e. M ( f supp Z ) C_ ( 0 ... m ) )
16	15	2a1d 27	. 2 |- ( ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) -> ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) -> ( A. f e. M f finSupp Z -> E. m e. NN0 A. f e. M ( f supp Z ) C_ ( 0 ... m ) ) ) )
17		simplr 760	. . . . 5 |- ( ( ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) /\ ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) ) /\ A. f e. M f finSupp Z ) -> ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) )
18		simpr 462	. . . . . 6 |- ( ( ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) /\ ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) ) /\ A. f e. M f finSupp Z ) -> A. f e. M f finSupp Z )
19		ioran 492	. . . . . . . . . 10 |- ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) <-> ( -. (/) = M /\ -. A. f e. M ( f supp Z ) = (/) ) )
20		oveq1 6304	. . . . . . . . . . . . . 14 |- ( f = g -> ( f supp Z ) = ( g supp Z ) )
21	20	eqeq1d 2422	. . . . . . . . . . . . 13 |- ( f = g -> ( ( f supp Z ) = (/) <-> ( g supp Z ) = (/) ) )
22	21	cbvralv 3053	. . . . . . . . . . . 12 |- ( A. f e. M ( f supp Z ) = (/) <-> A. g e. M ( g supp Z ) = (/) )
23	22	notbii 297	. . . . . . . . . . 11 |- ( -. A. f e. M ( f supp Z ) = (/) <-> -. A. g e. M ( g supp Z ) = (/) )
24	23	anbi2i 698	. . . . . . . . . 10 |- ( ( -. (/) = M /\ -. A. f e. M ( f supp Z ) = (/) ) <-> ( -. (/) = M /\ -. A. g e. M ( g supp Z ) = (/) ) )
25	19, 24	bitri 252	. . . . . . . . 9 |- ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) <-> ( -. (/) = M /\ -. A. g e. M ( g supp Z ) = (/) ) )
26		rexnal 2871	. . . . . . . . . . 11 |- ( E. g e. M -. ( g supp Z ) = (/) <-> -. A. g e. M ( g supp Z ) = (/) )
27		df-ne 2618	. . . . . . . . . . . . . 14 |- ( ( g supp Z ) =/= (/) <-> -. ( g supp Z ) = (/) )
28	27	bicomi 205	. . . . . . . . . . . . 13 |- ( -. ( g supp Z ) = (/) <-> ( g supp Z ) =/= (/) )
29	28	rexbii 2925	. . . . . . . . . . . 12 |- ( E. g e. M -. ( g supp Z ) = (/) <-> E. g e. M ( g supp Z ) =/= (/) )
30	29	biimpi 197	. . . . . . . . . . 11 |- ( E. g e. M -. ( g supp Z ) = (/) -> E. g e. M ( g supp Z ) =/= (/) )
31	26, 30	sylbir 216	. . . . . . . . . 10 |- ( -. A. g e. M ( g supp Z ) = (/) -> E. g e. M ( g supp Z ) =/= (/) )
32	31	adantl 467	. . . . . . . . 9 |- ( ( -. (/) = M /\ -. A. g e. M ( g supp Z ) = (/) ) -> E. g e. M ( g supp Z ) =/= (/) )
33	25, 32	sylbi 198	. . . . . . . 8 |- ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) -> E. g e. M ( g supp Z ) =/= (/) )
34	33	ad2antrr 730	. . . . . . 7 |- ( ( ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) /\ ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) ) /\ A. f e. M f finSupp Z ) -> E. g e. M ( g supp Z ) =/= (/) )
35		iunn0 4353	. . . . . . 7 |- ( E. g e. M ( g supp Z ) =/= (/) <-> U_ g e. M ( g supp Z ) =/= (/) )
36	34, 35	sylib 199	. . . . . 6 |- ( ( ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) /\ ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) ) /\ A. f e. M f finSupp Z ) -> U_ g e. M ( g supp Z ) =/= (/) )
37	18, 36	jca 534	. . . . 5 |- ( ( ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) /\ ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) ) /\ A. f e. M f finSupp Z ) -> ( A. f e. M f finSupp Z /\ U_ g e. M ( g supp Z ) =/= (/) ) )
38		oveq1 6304	. . . . . . 7 |- ( g = f -> ( g supp Z ) = ( f supp Z ) )
39	38	cbviunv 4332	. . . . . 6 |- U_ g e. M ( g supp Z ) = U_ f e. M ( f supp Z )
40		eqid 2420	. . . . . 6 |- sup ( U_ g e. M ( g supp Z ) , RR , < ) = sup ( U_ g e. M ( g supp Z ) , RR , < )
41	39, 40	fsuppmapnn0fiublem 12195	. . . . 5 |- ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) -> ( ( A. f e. M f finSupp Z /\ U_ g e. M ( g supp Z ) =/= (/) ) -> sup ( U_ g e. M ( g supp Z ) , RR , < ) e. NN0 ) )
42	17, 37, 41	sylc 62	. . . 4 |- ( ( ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) /\ ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) ) /\ A. f e. M f finSupp Z ) -> sup ( U_ g e. M ( g supp Z ) , RR , < ) e. NN0 )
43		nfv 1751	. . . . . . . . . 10 |- F/ f (/) = M
44		nfra1 2804	. . . . . . . . . 10 |- F/ f A. f e. M ( f supp Z ) = (/)
45	43, 44	nfor 1990	. . . . . . . . 9 |- F/ f ( (/) = M \/ A. f e. M ( f supp Z ) = (/) )
46	45	nfn 1955	. . . . . . . 8 |- F/ f -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) )
47		nfv 1751	. . . . . . . 8 |- F/ f ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V )
48	46, 47	nfan 1983	. . . . . . 7 |- F/ f ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) /\ ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) )
49		nfra1 2804	. . . . . . 7 |- F/ f A. f e. M f finSupp Z
50	48, 49	nfan 1983	. . . . . 6 |- F/ f ( ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) /\ ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) ) /\ A. f e. M f finSupp Z )
51		nfv 1751	. . . . . 6 |- F/ f m = sup ( U_ g e. M ( g supp Z ) , RR , < )
52	50, 51	nfan 1983	. . . . 5 |- F/ f ( ( ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) /\ ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) ) /\ A. f e. M f finSupp Z ) /\ m = sup ( U_ g e. M ( g supp Z ) , RR , < ) )
53		oveq2 6305	. . . . . . 7 |- ( m = sup ( U_ g e. M ( g supp Z ) , RR , < ) -> ( 0 ... m ) = ( 0 ... sup ( U_ g e. M ( g supp Z ) , RR , < ) ) )
54	53	sseq2d 3489	. . . . . 6 |- ( m = sup ( U_ g e. M ( g supp Z ) , RR , < ) -> ( ( f supp Z ) C_ ( 0 ... m ) <-> ( f supp Z ) C_ ( 0 ... sup ( U_ g e. M ( g supp Z ) , RR , < ) ) ) )
55	54	adantl 467	. . . . 5 |- ( ( ( ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) /\ ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) ) /\ A. f e. M f finSupp Z ) /\ m = sup ( U_ g e. M ( g supp Z ) , RR , < ) ) -> ( ( f supp Z ) C_ ( 0 ... m ) <-> ( f supp Z ) C_ ( 0 ... sup ( U_ g e. M ( g supp Z ) , RR , < ) ) ) )
56	52, 55	ralbid 2857	. . . 4 |- ( ( ( ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) /\ ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) ) /\ A. f e. M f finSupp Z ) /\ m = sup ( U_ g e. M ( g supp Z ) , RR , < ) ) -> ( A. f e. M ( f supp Z ) C_ ( 0 ... m ) <-> A. f e. M ( f supp Z ) C_ ( 0 ... sup ( U_ g e. M ( g supp Z ) , RR , < ) ) ) )
57		rexnal 2871	. . . . . . . . . . 11 |- ( E. f e. M -. ( f supp Z ) = (/) <-> -. A. f e. M ( f supp Z ) = (/) )
58		df-ne 2618	. . . . . . . . . . . . . 14 |- ( ( f supp Z ) =/= (/) <-> -. ( f supp Z ) = (/) )
59	58	bicomi 205	. . . . . . . . . . . . 13 |- ( -. ( f supp Z ) = (/) <-> ( f supp Z ) =/= (/) )
60	59	rexbii 2925	. . . . . . . . . . . 12 |- ( E. f e. M -. ( f supp Z ) = (/) <-> E. f e. M ( f supp Z ) =/= (/) )
61	60	biimpi 197	. . . . . . . . . . 11 |- ( E. f e. M -. ( f supp Z ) = (/) -> E. f e. M ( f supp Z ) =/= (/) )
62	57, 61	sylbir 216	. . . . . . . . . 10 |- ( -. A. f e. M ( f supp Z ) = (/) -> E. f e. M ( f supp Z ) =/= (/) )
63	62	adantl 467	. . . . . . . . 9 |- ( ( -. (/) = M /\ -. A. f e. M ( f supp Z ) = (/) ) -> E. f e. M ( f supp Z ) =/= (/) )
64	19, 63	sylbi 198	. . . . . . . 8 |- ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) -> E. f e. M ( f supp Z ) =/= (/) )
65	64	ad2antrr 730	. . . . . . 7 |- ( ( ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) /\ ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) ) /\ A. f e. M f finSupp Z ) -> E. f e. M ( f supp Z ) =/= (/) )
66		iunn0 4353	. . . . . . . 8 |- ( E. f e. M ( f supp Z ) =/= (/) <-> U_ f e. M ( f supp Z ) =/= (/) )
67	20	cbviunv 4332	. . . . . . . . 9 |- U_ f e. M ( f supp Z ) = U_ g e. M ( g supp Z )
68	67	neeq1i 2707	. . . . . . . 8 |- ( U_ f e. M ( f supp Z ) =/= (/) <-> U_ g e. M ( g supp Z ) =/= (/) )
69	66, 68	bitri 252	. . . . . . 7 |- ( E. f e. M ( f supp Z ) =/= (/) <-> U_ g e. M ( g supp Z ) =/= (/) )
70	65, 69	sylib 199	. . . . . 6 |- ( ( ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) /\ ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) ) /\ A. f e. M f finSupp Z ) -> U_ g e. M ( g supp Z ) =/= (/) )
71	18, 70	jca 534	. . . . 5 |- ( ( ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) /\ ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) ) /\ A. f e. M f finSupp Z ) -> ( A. f e. M f finSupp Z /\ U_ g e. M ( g supp Z ) =/= (/) ) )
72	39, 40	fsuppmapnn0fiub 12196	. . . . 5 |- ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) -> ( ( A. f e. M f finSupp Z /\ U_ g e. M ( g supp Z ) =/= (/) ) -> A. f e. M ( f supp Z ) C_ ( 0 ... sup ( U_ g e. M ( g supp Z ) , RR , < ) ) ) )
73	17, 71, 72	sylc 62	. . . 4 |- ( ( ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) /\ ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) ) /\ A. f e. M f finSupp Z ) -> A. f e. M ( f supp Z ) C_ ( 0 ... sup ( U_ g e. M ( g supp Z ) , RR , < ) ) )
74	42, 56, 73	rspcedvd 3184	. . 3 |- ( ( ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) /\ ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) ) /\ A. f e. M f finSupp Z ) -> E. m e. NN0 A. f e. M ( f supp Z ) C_ ( 0 ... m ) )
75	74	exp31 607	. 2 |- ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) -> ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) -> ( A. f e. M f finSupp Z -> E. m e. NN0 A. f e. M ( f supp Z ) C_ ( 0 ... m ) ) ) )
76	16, 75	pm2.61i 167	1 |- ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) -> ( A. f e. M f finSupp Z -> E. m e. NN0 A. f e. M ( f supp Z ) C_ ( 0 ... m ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   \/ wo 369   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1867   =/= wne 2616   A.wral 2773   E.wrex 2774   C_ wss 3433   (/)c0 3758   U_ciun 4293   class class class wbr 4417  (class class class)co 6297   supp csupp 6917   ^m cmap 7472   Fincfn 7569   finSupp cfsupp 7881   supcsup 7952   RRcr 9534   0cc0 9535   < clt 9671   NN0cn0 10865   ...cfz 11778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4540  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6589  ax-cnex 9591  ax-resscn 9592  ax-1cn 9593  ax-icn 9594  ax-addcl 9595  ax-addrcl 9596  ax-mulcl 9597  ax-mulrcl 9598  ax-mulcom 9599  ax-addass 9600  ax-mulass 9601  ax-distr 9602  ax-i2m1 9603  ax-1ne0 9604  ax-1rid 9605  ax-rnegex 9606  ax-rrecex 9607  ax-cnre 9608  ax-pre-lttri 9609  ax-pre-lttrn 9610  ax-pre-ltadd 9611  ax-pre-mulgt0 9612

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-nel 2619  df-ral 2778  df-rex 2779  df-reu 2780  df-rmo 2781  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-int 4250  df-iun 4295  df-br 4418  df-opab 4477  df-mpt 4478  df-tr 4513  df-eprel 4757  df-id 4761  df-po 4767  df-so 4768  df-fr 4805  df-we 4807  df-xp 4852  df-rel 4853  df-cnv 4854  df-co 4855  df-dm 4856  df-rn 4857  df-res 4858  df-ima 4859  df-pred 5391  df-ord 5437  df-on 5438  df-lim 5439  df-suc 5440  df-iota 5557  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6259  df-ov 6300  df-oprab 6301  df-mpt2 6302  df-om 6699  df-1st 6799  df-2nd 6800  df-supp 6918  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-1o 7182  df-oadd 7186  df-er 7363  df-map 7474  df-en 7570  df-dom 7571  df-sdom 7572  df-fin 7573  df-fsupp 7882  df-sup 7954  df-pnf 9673  df-mnf 9674  df-xr 9675  df-ltxr 9676  df-le 9677  df-sub 9858  df-neg 9859  df-nn 10606  df-n0 10866  df-z 10934  df-uz 11156  df-fz 11779

This theorem is referenced by:  fsuppmapnn0fiub0  12198