Theorem fsuppmapnn0fiubex 12052

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 10771	. . . . . 6 |- 0 e. NN0
2	1	a1i 11	. . . . 5 |- ( ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) -> 0 e. NN0 )
3		oveq2 6242	. . . . . . . 8 |- ( m = 0 -> ( 0 ... m ) = ( 0 ... 0 ) )
4	3	sseq2d 3469	. . . . . . 7 |- ( m = 0 -> ( ( f supp Z ) C_ ( 0 ... m ) <-> ( f supp Z ) C_ ( 0 ... 0 ) ) )
5	4	ralbidv 2842	. . . . . 6 |- ( 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 464	. . . . 5 |- ( ( ( (/) = 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 3877	. . . . . . 7 |- A. f e. (/) ( f supp Z ) C_ ( 0 ... 0 )
8		raleq 3003	. . . . . . 7 |- ( (/) = M -> ( A. f e. (/) ( f supp Z ) C_ ( 0 ... 0 ) <-> A. f e. M ( f supp Z ) C_ ( 0 ... 0 ) ) )
9	7, 8	mpbii 211	. . . . . 6 |- ( (/) = M -> A. f e. M ( f supp Z ) C_ ( 0 ... 0 ) )
10		0ss 3767	. . . . . . . 8 |- (/) C_ ( 0 ... 0 )
11		sseq1 3462	. . . . . . . 8 |- ( ( f supp Z ) = (/) -> ( ( f supp Z ) C_ ( 0 ... 0 ) <-> (/) C_ ( 0 ... 0 ) ) )
12	10, 11	mpbiri 233	. . . . . . 7 |- ( ( f supp Z ) = (/) -> ( f supp Z ) C_ ( 0 ... 0 ) )
13	12	ralimi 2796	. . . . . 6 |- ( A. f e. M ( f supp Z ) = (/) -> A. f e. M ( f supp Z ) C_ ( 0 ... 0 ) )
14	9, 13	jaoi 377	. . . . 5 |- ( ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) -> A. f e. M ( f supp Z ) C_ ( 0 ... 0 ) )
15	2, 6, 14	rspcedvd 3164	. . . 4 |- ( ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) -> E. m e. NN0 A. f e. M ( f supp Z ) C_ ( 0 ... m ) )
16	15	a1d 25	. . 3 |- ( ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) -> ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) -> E. m e. NN0 A. f e. M ( f supp Z ) C_ ( 0 ... m ) ) )
17	16	a1dd 44	. 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 ) ) ) )
18		simplr 754	. . . . 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 ) )
19		simpr 459	. . . . . 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 )
20		ioran 488	. . . . . . . . . 10 |- ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) <-> ( -. (/) = M /\ -. A. f e. M ( f supp Z ) = (/) ) )
21		oveq1 6241	. . . . . . . . . . . . . 14 |- ( f = g -> ( f supp Z ) = ( g supp Z ) )
22	21	eqeq1d 2404	. . . . . . . . . . . . 13 |- ( f = g -> ( ( f supp Z ) = (/) <-> ( g supp Z ) = (/) ) )
23	22	cbvralv 3033	. . . . . . . . . . . 12 |- ( A. f e. M ( f supp Z ) = (/) <-> A. g e. M ( g supp Z ) = (/) )
24	23	notbii 294	. . . . . . . . . . 11 |- ( -. A. f e. M ( f supp Z ) = (/) <-> -. A. g e. M ( g supp Z ) = (/) )
25	24	anbi2i 692	. . . . . . . . . 10 |- ( ( -. (/) = M /\ -. A. f e. M ( f supp Z ) = (/) ) <-> ( -. (/) = M /\ -. A. g e. M ( g supp Z ) = (/) ) )
26	20, 25	bitri 249	. . . . . . . . 9 |- ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) <-> ( -. (/) = M /\ -. A. g e. M ( g supp Z ) = (/) ) )
27		rexnal 2851	. . . . . . . . . . 11 |- ( E. g e. M -. ( g supp Z ) = (/) <-> -. A. g e. M ( g supp Z ) = (/) )
28		df-ne 2600	. . . . . . . . . . . . . 14 |- ( ( g supp Z ) =/= (/) <-> -. ( g supp Z ) = (/) )
29	28	bicomi 202	. . . . . . . . . . . . 13 |- ( -. ( g supp Z ) = (/) <-> ( g supp Z ) =/= (/) )
30	29	rexbii 2905	. . . . . . . . . . . 12 |- ( E. g e. M -. ( g supp Z ) = (/) <-> E. g e. M ( g supp Z ) =/= (/) )
31	30	biimpi 194	. . . . . . . . . . 11 |- ( E. g e. M -. ( g supp Z ) = (/) -> E. g e. M ( g supp Z ) =/= (/) )
32	27, 31	sylbir 213	. . . . . . . . . 10 |- ( -. A. g e. M ( g supp Z ) = (/) -> E. g e. M ( g supp Z ) =/= (/) )
33	32	adantl 464	. . . . . . . . 9 |- ( ( -. (/) = M /\ -. A. g e. M ( g supp Z ) = (/) ) -> E. g e. M ( g supp Z ) =/= (/) )
34	26, 33	sylbi 195	. . . . . . . 8 |- ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) -> E. g e. M ( g supp Z ) =/= (/) )
35	34	ad2antrr 724	. . . . . . 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 ) =/= (/) )
36		iunn0 4330	. . . . . . 7 |- ( E. g e. M ( g supp Z ) =/= (/) <-> U_ g e. M ( g supp Z ) =/= (/) )
37	35, 36	sylib 196	. . . . . 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 ) =/= (/) )
38	19, 37	jca 530	. . . . 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 ) =/= (/) ) )
39		oveq1 6241	. . . . . . 7 |- ( g = f -> ( g supp Z ) = ( f supp Z ) )
40	39	cbviunv 4309	. . . . . 6 |- U_ g e. M ( g supp Z ) = U_ f e. M ( f supp Z )
41		eqid 2402	. . . . . 6 |- sup ( U_ g e. M ( g supp Z ) , RR , < ) = sup ( U_ g e. M ( g supp Z ) , RR , < )
42	40, 41	fsuppmapnn0fiublem 12050	. . . . 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 ) )
43	18, 38, 42	sylc 59	. . . 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 )
44		nfv 1728	. . . . . . . . . 10 |- F/ f (/) = M
45		nfra1 2784	. . . . . . . . . 10 |- F/ f A. f e. M ( f supp Z ) = (/)
46	44, 45	nfor 1963	. . . . . . . . 9 |- F/ f ( (/) = M \/ A. f e. M ( f supp Z ) = (/) )
47	46	nfn 1929	. . . . . . . 8 |- F/ f -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) )
48		nfv 1728	. . . . . . . 8 |- F/ f ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V )
49	47, 48	nfan 1956	. . . . . . 7 |- F/ f ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) /\ ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) )
50		nfra1 2784	. . . . . . 7 |- F/ f A. f e. M f finSupp Z
51	49, 50	nfan 1956	. . . . . 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 )
52		nfv 1728	. . . . . 6 |- F/ f m = sup ( U_ g e. M ( g supp Z ) , RR , < )
53	51, 52	nfan 1956	. . . . 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 , < ) )
54		oveq2 6242	. . . . . . 7 |- ( m = sup ( U_ g e. M ( g supp Z ) , RR , < ) -> ( 0 ... m ) = ( 0 ... sup ( U_ g e. M ( g supp Z ) , RR , < ) ) )
55	54	sseq2d 3469	. . . . . 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 , < ) ) ) )
56	55	adantl 464	. . . . 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 , < ) ) ) )
57	53, 56	ralbid 2837	. . . 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 , < ) ) ) )
58		rexnal 2851	. . . . . . . . . . 11 |- ( E. f e. M -. ( f supp Z ) = (/) <-> -. A. f e. M ( f supp Z ) = (/) )
59		df-ne 2600	. . . . . . . . . . . . . 14 |- ( ( f supp Z ) =/= (/) <-> -. ( f supp Z ) = (/) )
60	59	bicomi 202	. . . . . . . . . . . . 13 |- ( -. ( f supp Z ) = (/) <-> ( f supp Z ) =/= (/) )
61	60	rexbii 2905	. . . . . . . . . . . 12 |- ( E. f e. M -. ( f supp Z ) = (/) <-> E. f e. M ( f supp Z ) =/= (/) )
62	61	biimpi 194	. . . . . . . . . . 11 |- ( E. f e. M -. ( f supp Z ) = (/) -> E. f e. M ( f supp Z ) =/= (/) )
63	58, 62	sylbir 213	. . . . . . . . . 10 |- ( -. A. f e. M ( f supp Z ) = (/) -> E. f e. M ( f supp Z ) =/= (/) )
64	63	adantl 464	. . . . . . . . 9 |- ( ( -. (/) = M /\ -. A. f e. M ( f supp Z ) = (/) ) -> E. f e. M ( f supp Z ) =/= (/) )
65	20, 64	sylbi 195	. . . . . . . 8 |- ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) -> E. f e. M ( f supp Z ) =/= (/) )
66	65	ad2antrr 724	. . . . . . 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 ) =/= (/) )
67		iunn0 4330	. . . . . . . 8 |- ( E. f e. M ( f supp Z ) =/= (/) <-> U_ f e. M ( f supp Z ) =/= (/) )
68	21	cbviunv 4309	. . . . . . . . 9 |- U_ f e. M ( f supp Z ) = U_ g e. M ( g supp Z )
69	68	neeq1i 2688	. . . . . . . 8 |- ( U_ f e. M ( f supp Z ) =/= (/) <-> U_ g e. M ( g supp Z ) =/= (/) )
70	67, 69	bitri 249	. . . . . . 7 |- ( E. f e. M ( f supp Z ) =/= (/) <-> U_ g e. M ( g supp Z ) =/= (/) )
71	66, 70	sylib 196	. . . . . 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 ) =/= (/) )
72	19, 71	jca 530	. . . . 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 ) =/= (/) ) )
73	40, 41	fsuppmapnn0fiub 12051	. . . . 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 , < ) ) ) )
74	18, 72, 73	sylc 59	. . . 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 , < ) ) )
75	43, 57, 74	rspcedvd 3164	. . 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 ) )
76	75	exp31 602	. 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 ) ) ) )
77	17, 76	pm2.61i 164	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 184   \/ wo 366   /\ wa 367   /\ w3a 974   = wceq 1405   e. wcel 1842   =/= wne 2598   A.wral 2753   E.wrex 2754   C_ wss 3413   (/)c0 3737   U_ciun 4270   class class class wbr 4394  (class class class)co 6234   supp csupp 6856   ^m cmap 7377   Fincfn 7474   finSupp cfsupp 7783   supcsup 7854   RRcr 9441   0cc0 9442   < clt 9578   NN0cn0 10756   ...cfz 11643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6530  ax-cnex 9498  ax-resscn 9499  ax-1cn 9500  ax-icn 9501  ax-addcl 9502  ax-addrcl 9503  ax-mulcl 9504  ax-mulrcl 9505  ax-mulcom 9506  ax-addass 9507  ax-mulass 9508  ax-distr 9509  ax-i2m1 9510  ax-1ne0 9511  ax-1rid 9512  ax-rnegex 9513  ax-rrecex 9514  ax-cnre 9515  ax-pre-lttri 9516  ax-pre-lttrn 9517  ax-pre-ltadd 9518  ax-pre-mulgt0 9519

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2758  df-rex 2759  df-reu 2760  df-rmo 2761  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-pss 3429  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-tp 3976  df-op 3978  df-uni 4191  df-int 4227  df-iun 4272  df-br 4395  df-opab 4453  df-mpt 4454  df-tr 4489  df-eprel 4733  df-id 4737  df-po 4743  df-so 4744  df-fr 4781  df-we 4783  df-ord 4824  df-on 4825  df-lim 4826  df-suc 4827  df-xp 4948  df-rel 4949  df-cnv 4950  df-co 4951  df-dm 4952  df-rn 4953  df-res 4954  df-ima 4955  df-iota 5489  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-riota 6196  df-ov 6237  df-oprab 6238  df-mpt2 6239  df-om 6639  df-1st 6738  df-2nd 6739  df-supp 6857  df-recs 6999  df-rdg 7033  df-1o 7087  df-oadd 7091  df-er 7268  df-map 7379  df-en 7475  df-dom 7476  df-sdom 7477  df-fin 7478  df-fsupp 7784  df-sup 7855  df-pnf 9580  df-mnf 9581  df-xr 9582  df-ltxr 9583  df-le 9584  df-sub 9763  df-neg 9764  df-nn 10497  df-n0 10757  df-z 10826  df-uz 11046  df-fz 11644

This theorem is referenced by:  fsuppmapnn0fiub0  12053