Metamath Proof Explorer

Theorem uzfissfz

Description: For any finite subset of the upper integers, there is a finite set of sequential integers that includes it. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses uzfissfz.m 
|- ( ph -> M e. ZZ )
uzfissfz.z 
|- Z = ( ZZ>= ` M )
uzfissfz.a 
|- ( ph -> A C_ Z )
uzfissfz.fi 
|- ( ph -> A e. Fin )
Assertion uzfissfz 
|- ( ph -> E. k e. Z A C_ ( M ... k ) )

Proof

Step Hyp Ref Expression
1 uzfissfz.m 
 |-  ( ph -> M e. ZZ )
2 uzfissfz.z 
 |-  Z = ( ZZ>= ` M )
3 uzfissfz.a 
 |-  ( ph -> A C_ Z )
4 uzfissfz.fi 
 |-  ( ph -> A e. Fin )
5 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
6 1 5 syl 
 |-  ( ph -> M e. ( ZZ>= ` M ) )
7 2 a1i 
 |-  ( ph -> Z = ( ZZ>= ` M ) )
8 7 eqcomd 
 |-  ( ph -> ( ZZ>= ` M ) = Z )
9 6 8 eleqtrd 
 |-  ( ph -> M e. Z )
10 9 adantr 
 |-  ( ( ph /\ A = (/) ) -> M e. Z )
11 id 
 |-  ( A = (/) -> A = (/) )
12 0ss 
 |-  (/) C_ ( M ... M )
13 12 a1i 
 |-  ( A = (/) -> (/) C_ ( M ... M ) )
14 11 13 eqsstrd 
 |-  ( A = (/) -> A C_ ( M ... M ) )
15 14 adantl 
 |-  ( ( ph /\ A = (/) ) -> A C_ ( M ... M ) )
16 oveq2 
 |-  ( k = M -> ( M ... k ) = ( M ... M ) )
17 16 sseq2d 
 |-  ( k = M -> ( A C_ ( M ... k ) <-> A C_ ( M ... M ) ) )
18 17 rspcev 
 |-  ( ( M e. Z /\ A C_ ( M ... M ) ) -> E. k e. Z A C_ ( M ... k ) )
19 10 15 18 syl2anc 
 |-  ( ( ph /\ A = (/) ) -> E. k e. Z A C_ ( M ... k ) )
20 3 adantr 
 |-  ( ( ph /\ -. A = (/) ) -> A C_ Z )
21 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
22 2 21 eqsstri 
 |-  Z C_ ZZ
23 22 a1i 
 |-  ( ph -> Z C_ ZZ )
24 3 23 sstrd 
 |-  ( ph -> A C_ ZZ )
25 24 adantr 
 |-  ( ( ph /\ -. A = (/) ) -> A C_ ZZ )
26 11 necon3bi 
 |-  ( -. A = (/) -> A =/= (/) )
27 26 adantl 
 |-  ( ( ph /\ -. A = (/) ) -> A =/= (/) )
28 4 adantr 
 |-  ( ( ph /\ -. A = (/) ) -> A e. Fin )
29 suprfinzcl 
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ A e. Fin ) -> sup ( A , RR , < ) e. A )
30 25 27 28 29 syl3anc 
 |-  ( ( ph /\ -. A = (/) ) -> sup ( A , RR , < ) e. A )
31 20 30 sseldd 
 |-  ( ( ph /\ -. A = (/) ) -> sup ( A , RR , < ) e. Z )
32 1 ad2antrr 
 |-  ( ( ( ph /\ -. A = (/) ) /\ j e. A ) -> M e. ZZ )
33 22 31 sseldi 
 |-  ( ( ph /\ -. A = (/) ) -> sup ( A , RR , < ) e. ZZ )
34 33 adantr 
 |-  ( ( ( ph /\ -. A = (/) ) /\ j e. A ) -> sup ( A , RR , < ) e. ZZ )
35 25 sselda 
 |-  ( ( ( ph /\ -. A = (/) ) /\ j e. A ) -> j e. ZZ )
36 32 34 35 3jca 
 |-  ( ( ( ph /\ -. A = (/) ) /\ j e. A ) -> ( M e. ZZ /\ sup ( A , RR , < ) e. ZZ /\ j e. ZZ ) )
37 3 sselda 
 |-  ( ( ph /\ j e. A ) -> j e. Z )
38 2 a1i 
 |-  ( ( ph /\ j e. A ) -> Z = ( ZZ>= ` M ) )
39 37 38 eleqtrd 
 |-  ( ( ph /\ j e. A ) -> j e. ( ZZ>= ` M ) )
40 eluzle 
 |-  ( j e. ( ZZ>= ` M ) -> M <_ j )
41 39 40 syl 
 |-  ( ( ph /\ j e. A ) -> M <_ j )
42 41 adantlr 
 |-  ( ( ( ph /\ -. A = (/) ) /\ j e. A ) -> M <_ j )
43 zssre 
 |-  ZZ C_ RR
44 24 43 sstrdi 
 |-  ( ph -> A C_ RR )
45 44 ad2antrr 
 |-  ( ( ( ph /\ -. A = (/) ) /\ j e. A ) -> A C_ RR )
46 27 adantr 
 |-  ( ( ( ph /\ -. A = (/) ) /\ j e. A ) -> A =/= (/) )
47 fimaxre2 
 |-  ( ( A C_ RR /\ A e. Fin ) -> E. x e. RR A. y e. A y <_ x )
48 44 4 47 syl2anc 
 |-  ( ph -> E. x e. RR A. y e. A y <_ x )
49 48 ad2antrr 
 |-  ( ( ( ph /\ -. A = (/) ) /\ j e. A ) -> E. x e. RR A. y e. A y <_ x )
50 simpr 
 |-  ( ( ( ph /\ -. A = (/) ) /\ j e. A ) -> j e. A )
51 suprub 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ j e. A ) -> j <_ sup ( A , RR , < ) )
52 45 46 49 50 51 syl31anc 
 |-  ( ( ( ph /\ -. A = (/) ) /\ j e. A ) -> j <_ sup ( A , RR , < ) )
53 36 42 52 jca32 
 |-  ( ( ( ph /\ -. A = (/) ) /\ j e. A ) -> ( ( M e. ZZ /\ sup ( A , RR , < ) e. ZZ /\ j e. ZZ ) /\ ( M <_ j /\ j <_ sup ( A , RR , < ) ) ) )
54 elfz2 
 |-  ( j e. ( M ... sup ( A , RR , < ) ) <-> ( ( M e. ZZ /\ sup ( A , RR , < ) e. ZZ /\ j e. ZZ ) /\ ( M <_ j /\ j <_ sup ( A , RR , < ) ) ) )
55 53 54 sylibr 
 |-  ( ( ( ph /\ -. A = (/) ) /\ j e. A ) -> j e. ( M ... sup ( A , RR , < ) ) )
56 55 ralrimiva 
 |-  ( ( ph /\ -. A = (/) ) -> A. j e. A j e. ( M ... sup ( A , RR , < ) ) )
57 dfss3 
 |-  ( A C_ ( M ... sup ( A , RR , < ) ) <-> A. j e. A j e. ( M ... sup ( A , RR , < ) ) )
58 56 57 sylibr 
 |-  ( ( ph /\ -. A = (/) ) -> A C_ ( M ... sup ( A , RR , < ) ) )
59 oveq2 
 |-  ( k = sup ( A , RR , < ) -> ( M ... k ) = ( M ... sup ( A , RR , < ) ) )
60 59 sseq2d 
 |-  ( k = sup ( A , RR , < ) -> ( A C_ ( M ... k ) <-> A C_ ( M ... sup ( A , RR , < ) ) ) )
61 60 rspcev 
 |-  ( ( sup ( A , RR , < ) e. Z /\ A C_ ( M ... sup ( A , RR , < ) ) ) -> E. k e. Z A C_ ( M ... k ) )
62 31 58 61 syl2anc 
 |-  ( ( ph /\ -. A = (/) ) -> E. k e. Z A C_ ( M ... k ) )
63 19 62 pm2.61dan 
 |-  ( ph -> E. k e. Z A C_ ( M ... k ) )