This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 sselid 
 |-  ( ( 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 3 sselda 
 |-  ( ( ph /\ j e. A ) -> j e. Z )
37 2 a1i 
 |-  ( ( ph /\ j e. A ) -> Z = ( ZZ>= ` M ) )
38 36 37 eleqtrd 
 |-  ( ( ph /\ j e. A ) -> j e. ( ZZ>= ` M ) )
39 eluzle 
 |-  ( j e. ( ZZ>= ` M ) -> M <_ j )
40 38 39 syl 
 |-  ( ( ph /\ j e. A ) -> M <_ j )
41 40 adantlr 
 |-  ( ( ( ph /\ -. A = (/) ) /\ j e. A ) -> M <_ j )
42 zssre 
 |-  ZZ C_ RR
43 24 42 sstrdi 
 |-  ( ph -> A C_ RR )
44 43 ad2antrr 
 |-  ( ( ( ph /\ -. A = (/) ) /\ j e. A ) -> A C_ RR )
45 27 adantr 
 |-  ( ( ( ph /\ -. A = (/) ) /\ j e. A ) -> A =/= (/) )
46 fimaxre2 
 |-  ( ( A C_ RR /\ A e. Fin ) -> E. x e. RR A. y e. A y <_ x )
47 43 4 46 syl2anc 
 |-  ( ph -> E. x e. RR A. y e. A y <_ x )
48 47 ad2antrr 
 |-  ( ( ( ph /\ -. A = (/) ) /\ j e. A ) -> E. x e. RR A. y e. A y <_ x )
49 simpr 
 |-  ( ( ( ph /\ -. A = (/) ) /\ j e. A ) -> j e. A )
50 suprub 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ j e. A ) -> j <_ sup ( A , RR , < ) )
51 44 45 48 49 50 syl31anc 
 |-  ( ( ( ph /\ -. A = (/) ) /\ j e. A ) -> j <_ sup ( A , RR , < ) )
52 32 34 35 41 51 elfzd 
 |-  ( ( ( ph /\ -. A = (/) ) /\ j e. A ) -> j e. ( M ... sup ( A , RR , < ) ) )
53 52 ralrimiva 
 |-  ( ( ph /\ -. A = (/) ) -> A. j e. A j e. ( M ... sup ( A , RR , < ) ) )
54 dfss3 
 |-  ( A C_ ( M ... sup ( A , RR , < ) ) <-> A. j e. A j e. ( M ... sup ( A , RR , < ) ) )
55 53 54 sylibr 
 |-  ( ( ph /\ -. A = (/) ) -> A C_ ( M ... sup ( A , RR , < ) ) )
56 oveq2 
 |-  ( k = sup ( A , RR , < ) -> ( M ... k ) = ( M ... sup ( A , RR , < ) ) )
57 56 sseq2d 
 |-  ( k = sup ( A , RR , < ) -> ( A C_ ( M ... k ) <-> A C_ ( M ... sup ( A , RR , < ) ) ) )
58 57 rspcev 
 |-  ( ( sup ( A , RR , < ) e. Z /\ A C_ ( M ... sup ( A , RR , < ) ) ) -> E. k e. Z A C_ ( M ... k ) )
59 31 55 58 syl2anc 
 |-  ( ( ph /\ -. A = (/) ) -> E. k e. Z A C_ ( M ... k ) )
60 19 59 pm2.61dan 
 |-  ( ph -> E. k e. Z A C_ ( M ... k ) )