Metamath Proof Explorer

Theorem fsuppmapnn0fiub

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 and ending with the supremum of the union of the support of these functions. (Contributed by AV, 2-Oct-2019) (Proof shortened by JJ, 2-Aug-2021)

Ref Expression
Hypotheses fsuppmapnn0fiub.u 
|- U = U_ f e. M ( f supp Z )
fsuppmapnn0fiub.s 
|- S = sup ( U , RR , < )
Assertion fsuppmapnn0fiub 
|- ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) -> ( ( A. f e. M f finSupp Z /\ U =/= (/) ) -> A. f e. M ( f supp Z ) C_ ( 0 ... S ) ) )

Proof

Step Hyp Ref Expression
1 fsuppmapnn0fiub.u 
 |-  U = U_ f e. M ( f supp Z )
2 fsuppmapnn0fiub.s 
 |-  S = sup ( U , RR , < )
3 nfv 
 |-  F/ f ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V )
4 nfra1 
 |-  F/ f A. f e. M f finSupp Z
5 nfv 
 |-  F/ f U =/= (/)
6 4 5 nfan 
 |-  F/ f ( A. f e. M f finSupp Z /\ U =/= (/) )
7 3 6 nfan 
 |-  F/ f ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) )
8 suppssdm 
 |-  ( f supp Z ) C_ dom f
9 ssel2 
 |-  ( ( M C_ ( R ^m NN0 ) /\ f e. M ) -> f e. ( R ^m NN0 ) )
10 elmapfn 
 |-  ( f e. ( R ^m NN0 ) -> f Fn NN0 )
11 fndm 
 |-  ( f Fn NN0 -> dom f = NN0 )
12 eqimss 
 |-  ( dom f = NN0 -> dom f C_ NN0 )
13 11 12 syl 
 |-  ( f Fn NN0 -> dom f C_ NN0 )
14 9 10 13 3syl 
 |-  ( ( M C_ ( R ^m NN0 ) /\ f e. M ) -> dom f C_ NN0 )
15 14 3ad2antl1 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ f e. M ) -> dom f C_ NN0 )
16 8 15 sstrid 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ f e. M ) -> ( f supp Z ) C_ NN0 )
17 16 sseld 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ f e. M ) -> ( x e. ( f supp Z ) -> x e. NN0 ) )
18 17 adantlr 
 |-  ( ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) /\ f e. M ) -> ( x e. ( f supp Z ) -> x e. NN0 ) )
19 18 imp 
 |-  ( ( ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) /\ f e. M ) /\ x e. ( f supp Z ) ) -> x e. NN0 )
20 1 2 fsuppmapnn0fiublem 
 |-  ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) -> ( ( A. f e. M f finSupp Z /\ U =/= (/) ) -> S e. NN0 ) )
21 20 imp 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) -> S e. NN0 )
22 21 ad2antrr 
 |-  ( ( ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) /\ f e. M ) /\ x e. ( f supp Z ) ) -> S e. NN0 )
23 9 10 11 3syl 
 |-  ( ( M C_ ( R ^m NN0 ) /\ f e. M ) -> dom f = NN0 )
24 23 ex 
 |-  ( M C_ ( R ^m NN0 ) -> ( f e. M -> dom f = NN0 ) )
25 24 3ad2ant1 
 |-  ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) -> ( f e. M -> dom f = NN0 ) )
26 25 adantr 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) -> ( f e. M -> dom f = NN0 ) )
27 26 imp 
 |-  ( ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) /\ f e. M ) -> dom f = NN0 )
28 nn0ssre 
 |-  NN0 C_ RR
29 27 28 eqsstrdi 
 |-  ( ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) /\ f e. M ) -> dom f C_ RR )
30 8 29 sstrid 
 |-  ( ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) /\ f e. M ) -> ( f supp Z ) C_ RR )
31 30 ex 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) -> ( f e. M -> ( f supp Z ) C_ RR ) )
32 7 31 ralrimi 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) -> A. f e. M ( f supp Z ) C_ RR )
33 32 ad2antrr 
 |-  ( ( ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) /\ f e. M ) /\ x e. ( f supp Z ) ) -> A. f e. M ( f supp Z ) C_ RR )
34 iunss 
 |-  ( U_ f e. M ( f supp Z ) C_ RR <-> A. f e. M ( f supp Z ) C_ RR )
35 33 34 sylibr 
 |-  ( ( ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) /\ f e. M ) /\ x e. ( f supp Z ) ) -> U_ f e. M ( f supp Z ) C_ RR )
36 1 35 eqsstrid 
 |-  ( ( ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) /\ f e. M ) /\ x e. ( f supp Z ) ) -> U C_ RR )
37 simp2 
 |-  ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) -> M e. Fin )
38 id 
 |-  ( f finSupp Z -> f finSupp Z )
39 38 fsuppimpd 
 |-  ( f finSupp Z -> ( f supp Z ) e. Fin )
40 39 ralimi 
 |-  ( A. f e. M f finSupp Z -> A. f e. M ( f supp Z ) e. Fin )
41 40 adantr 
 |-  ( ( A. f e. M f finSupp Z /\ U =/= (/) ) -> A. f e. M ( f supp Z ) e. Fin )
42 37 41 anim12i 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) -> ( M e. Fin /\ A. f e. M ( f supp Z ) e. Fin ) )
43 42 ad2antrr 
 |-  ( ( ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) /\ f e. M ) /\ x e. ( f supp Z ) ) -> ( M e. Fin /\ A. f e. M ( f supp Z ) e. Fin ) )
44 iunfi 
 |-  ( ( M e. Fin /\ A. f e. M ( f supp Z ) e. Fin ) -> U_ f e. M ( f supp Z ) e. Fin )
45 43 44 syl 
 |-  ( ( ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) /\ f e. M ) /\ x e. ( f supp Z ) ) -> U_ f e. M ( f supp Z ) e. Fin )
46 1 45 eqeltrid 
 |-  ( ( ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) /\ f e. M ) /\ x e. ( f supp Z ) ) -> U e. Fin )
47 rspe 
 |-  ( ( f e. M /\ x e. ( f supp Z ) ) -> E. f e. M x e. ( f supp Z ) )
48 eliun 
 |-  ( x e. U_ f e. M ( f supp Z ) <-> E. f e. M x e. ( f supp Z ) )
49 47 48 sylibr 
 |-  ( ( f e. M /\ x e. ( f supp Z ) ) -> x e. U_ f e. M ( f supp Z ) )
50 49 1 eleqtrrdi 
 |-  ( ( f e. M /\ x e. ( f supp Z ) ) -> x e. U )
51 50 adantll 
 |-  ( ( ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) /\ f e. M ) /\ x e. ( f supp Z ) ) -> x e. U )
52 2 a1i 
 |-  ( ( ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) /\ f e. M ) /\ x e. ( f supp Z ) ) -> S = sup ( U , RR , < ) )
53 36 46 51 52 supfirege 
 |-  ( ( ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) /\ f e. M ) /\ x e. ( f supp Z ) ) -> x <_ S )
54 elfz2nn0 
 |-  ( x e. ( 0 ... S ) <-> ( x e. NN0 /\ S e. NN0 /\ x <_ S ) )
55 19 22 53 54 syl3anbrc 
 |-  ( ( ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) /\ f e. M ) /\ x e. ( f supp Z ) ) -> x e. ( 0 ... S ) )
56 55 ex 
 |-  ( ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) /\ f e. M ) -> ( x e. ( f supp Z ) -> x e. ( 0 ... S ) ) )
57 56 ssrdv 
 |-  ( ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) /\ f e. M ) -> ( f supp Z ) C_ ( 0 ... S ) )
58 57 ex 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) -> ( f e. M -> ( f supp Z ) C_ ( 0 ... S ) ) )
59 7 58 ralrimi 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) -> A. f e. M ( f supp Z ) C_ ( 0 ... S ) )
60 59 ex 
 |-  ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) -> ( ( A. f e. M f finSupp Z /\ U =/= (/) ) -> A. f e. M ( f supp Z ) C_ ( 0 ... S ) ) )