Metamath Proof Explorer

Theorem fsuppmapnn0fiubex

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)

Ref Expression
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 0nn0 
 |-  0 e. NN0
2 1 a1i 
 |-  ( ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) -> 0 e. NN0 )
3 oveq2 
 |-  ( m = 0 -> ( 0 ... m ) = ( 0 ... 0 ) )
4 3 sseq2d 
 |-  ( m = 0 -> ( ( f supp Z ) C_ ( 0 ... m ) <-> ( f supp Z ) C_ ( 0 ... 0 ) ) )
5 4 ralbidv 
 |-  ( 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 
 |-  ( ( ( (/) = 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 
 |-  A. f e. (/) ( f supp Z ) C_ ( 0 ... 0 )
8 raleq 
 |-  ( (/) = M -> ( A. f e. (/) ( f supp Z ) C_ ( 0 ... 0 ) <-> A. f e. M ( f supp Z ) C_ ( 0 ... 0 ) ) )
9 7 8 mpbii 
 |-  ( (/) = M -> A. f e. M ( f supp Z ) C_ ( 0 ... 0 ) )
10 0ss 
 |-  (/) C_ ( 0 ... 0 )
11 sseq1 
 |-  ( ( f supp Z ) = (/) -> ( ( f supp Z ) C_ ( 0 ... 0 ) <-> (/) C_ ( 0 ... 0 ) ) )
12 10 11 mpbiri 
 |-  ( ( f supp Z ) = (/) -> ( f supp Z ) C_ ( 0 ... 0 ) )
13 12 ralimi 
 |-  ( A. f e. M ( f supp Z ) = (/) -> A. f e. M ( f supp Z ) C_ ( 0 ... 0 ) )
14 9 13 jaoi 
 |-  ( ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) -> A. f e. M ( f supp Z ) C_ ( 0 ... 0 ) )
15 2 6 14 rspcedvd 
 |-  ( ( (/) = 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 
 |-  ( ( (/) = 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 
 |-  ( ( ( -. ( (/) = 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 
 |-  ( ( ( -. ( (/) = 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 
 |-  ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) <-> ( -. (/) = M /\ -. A. f e. M ( f supp Z ) = (/) ) )
20 oveq1 
 |-  ( f = g -> ( f supp Z ) = ( g supp Z ) )
21 20 eqeq1d 
 |-  ( f = g -> ( ( f supp Z ) = (/) <-> ( g supp Z ) = (/) ) )
22 21 cbvralvw 
 |-  ( A. f e. M ( f supp Z ) = (/) <-> A. g e. M ( g supp Z ) = (/) )
23 22 notbii 
 |-  ( -. A. f e. M ( f supp Z ) = (/) <-> -. A. g e. M ( g supp Z ) = (/) )
24 23 anbi2i 
 |-  ( ( -. (/) = M /\ -. A. f e. M ( f supp Z ) = (/) ) <-> ( -. (/) = M /\ -. A. g e. M ( g supp Z ) = (/) ) )
25 19 24 bitri 
 |-  ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) <-> ( -. (/) = M /\ -. A. g e. M ( g supp Z ) = (/) ) )
26 rexnal 
 |-  ( E. g e. M -. ( g supp Z ) = (/) <-> -. A. g e. M ( g supp Z ) = (/) )
27 df-ne 
 |-  ( ( g supp Z ) =/= (/) <-> -. ( g supp Z ) = (/) )
28 27 bicomi 
 |-  ( -. ( g supp Z ) = (/) <-> ( g supp Z ) =/= (/) )
29 28 rexbii 
 |-  ( E. g e. M -. ( g supp Z ) = (/) <-> E. g e. M ( g supp Z ) =/= (/) )
30 26 29 sylbb1 
 |-  ( -. A. g e. M ( g supp Z ) = (/) -> E. g e. M ( g supp Z ) =/= (/) )
31 25 30 simplbiim 
 |-  ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) -> E. g e. M ( g supp Z ) =/= (/) )
32 31 ad2antrr 
 |-  ( ( ( -. ( (/) = 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 ) =/= (/) )
33 iunn0 
 |-  ( E. g e. M ( g supp Z ) =/= (/) <-> U_ g e. M ( g supp Z ) =/= (/) )
34 32 33 sylib 
 |-  ( ( ( -. ( (/) = 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 ) =/= (/) )
35 18 34 jca 
 |-  ( ( ( -. ( (/) = 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 ) =/= (/) ) )
36 oveq1 
 |-  ( g = f -> ( g supp Z ) = ( f supp Z ) )
37 36 cbviunv 
 |-  U_ g e. M ( g supp Z ) = U_ f e. M ( f supp Z )
38 eqid 
 |-  sup ( U_ g e. M ( g supp Z ) , RR , < ) = sup ( U_ g e. M ( g supp Z ) , RR , < )
39 37 38 fsuppmapnn0fiublem 
 |-  ( ( 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 ) )
40 17 35 39 sylc 
 |-  ( ( ( -. ( (/) = 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 )
41 nfv 
 |-  F/ f (/) = M
42 nfra1 
 |-  F/ f A. f e. M ( f supp Z ) = (/)
43 41 42 nfor 
 |-  F/ f ( (/) = M \/ A. f e. M ( f supp Z ) = (/) )
44 43 nfn 
 |-  F/ f -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) )
45 nfv 
 |-  F/ f ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V )
46 44 45 nfan 
 |-  F/ f ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) /\ ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) )
47 nfra1 
 |-  F/ f A. f e. M f finSupp Z
48 46 47 nfan 
 |-  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 )
49 nfv 
 |-  F/ f m = sup ( U_ g e. M ( g supp Z ) , RR , < )
50 48 49 nfan 
 |-  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 , < ) )
51 oveq2 
 |-  ( m = sup ( U_ g e. M ( g supp Z ) , RR , < ) -> ( 0 ... m ) = ( 0 ... sup ( U_ g e. M ( g supp Z ) , RR , < ) ) )
52 51 sseq2d 
 |-  ( 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 , < ) ) ) )
53 52 adantl 
 |-  ( ( ( ( -. ( (/) = 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 , < ) ) ) )
54 50 53 ralbid 
 |-  ( ( ( ( -. ( (/) = 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 , < ) ) ) )
55 rexnal 
 |-  ( E. f e. M -. ( f supp Z ) = (/) <-> -. A. f e. M ( f supp Z ) = (/) )
56 df-ne 
 |-  ( ( f supp Z ) =/= (/) <-> -. ( f supp Z ) = (/) )
57 56 bicomi 
 |-  ( -. ( f supp Z ) = (/) <-> ( f supp Z ) =/= (/) )
58 57 rexbii 
 |-  ( E. f e. M -. ( f supp Z ) = (/) <-> E. f e. M ( f supp Z ) =/= (/) )
59 55 58 sylbb1 
 |-  ( -. A. f e. M ( f supp Z ) = (/) -> E. f e. M ( f supp Z ) =/= (/) )
60 19 59 simplbiim 
 |-  ( -. ( (/) = M \/ A. f e. M ( f supp Z ) = (/) ) -> E. f e. M ( f supp Z ) =/= (/) )
61 60 ad2antrr 
 |-  ( ( ( -. ( (/) = 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 ) =/= (/) )
62 iunn0 
 |-  ( E. f e. M ( f supp Z ) =/= (/) <-> U_ f e. M ( f supp Z ) =/= (/) )
63 20 cbviunv 
 |-  U_ f e. M ( f supp Z ) = U_ g e. M ( g supp Z )
64 63 neeq1i 
 |-  ( U_ f e. M ( f supp Z ) =/= (/) <-> U_ g e. M ( g supp Z ) =/= (/) )
65 62 64 bitri 
 |-  ( E. f e. M ( f supp Z ) =/= (/) <-> U_ g e. M ( g supp Z ) =/= (/) )
66 61 65 sylib 
 |-  ( ( ( -. ( (/) = 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 ) =/= (/) )
67 18 66 jca 
 |-  ( ( ( -. ( (/) = 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 ) =/= (/) ) )
68 37 38 fsuppmapnn0fiub 
 |-  ( ( 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 , < ) ) ) )
69 17 67 68 sylc 
 |-  ( ( ( -. ( (/) = 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 , < ) ) )
70 40 54 69 rspcedvd 
 |-  ( ( ( -. ( (/) = 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 ) )
71 70 exp31 
 |-  ( -. ( (/) = 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 ) ) ) )
72 16 71 pm2.61i 
 |-  ( ( 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 ) ) )