Metamath Proof Explorer

Theorem ssuzfz

Description: A finite subset of the upper integers is a subset of a finite set of sequential integers. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses ssuzfz.1 
|- Z = ( ZZ>= ` M )
ssuzfz.2 
|- ( ph -> A C_ Z )
ssuzfz.3 
|- ( ph -> A e. Fin )
Assertion ssuzfz 
|- ( ph -> A C_ ( M ... sup ( A , RR , < ) ) )

Proof

Step Hyp Ref Expression
1 ssuzfz.1 
 |-  Z = ( ZZ>= ` M )
2 ssuzfz.2 
 |-  ( ph -> A C_ Z )
3 ssuzfz.3 
 |-  ( ph -> A e. Fin )
4 2 sselda 
 |-  ( ( ph /\ k e. A ) -> k e. Z )
5 4 1 eleqtrdi 
 |-  ( ( ph /\ k e. A ) -> k e. ( ZZ>= ` M ) )
6 eluzel2 
 |-  ( k e. ( ZZ>= ` M ) -> M e. ZZ )
7 5 6 syl 
 |-  ( ( ph /\ k e. A ) -> M e. ZZ )
8 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
9 1 8 eqsstri 
 |-  Z C_ ZZ
10 9 a1i 
 |-  ( ph -> Z C_ ZZ )
11 2 10 sstrd 
 |-  ( ph -> A C_ ZZ )
12 11 adantr 
 |-  ( ( ph /\ k e. A ) -> A C_ ZZ )
13 ne0i 
 |-  ( k e. A -> A =/= (/) )
14 13 adantl 
 |-  ( ( ph /\ k e. A ) -> A =/= (/) )
15 3 adantr 
 |-  ( ( ph /\ k e. A ) -> A e. Fin )
16 suprfinzcl 
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ A e. Fin ) -> sup ( A , RR , < ) e. A )
17 12 14 15 16 syl3anc 
 |-  ( ( ph /\ k e. A ) -> sup ( A , RR , < ) e. A )
18 12 17 sseldd 
 |-  ( ( ph /\ k e. A ) -> sup ( A , RR , < ) e. ZZ )
19 11 sselda 
 |-  ( ( ph /\ k e. A ) -> k e. ZZ )
20 7 18 19 3jca 
 |-  ( ( ph /\ k e. A ) -> ( M e. ZZ /\ sup ( A , RR , < ) e. ZZ /\ k e. ZZ ) )
21 eluzle 
 |-  ( k e. ( ZZ>= ` M ) -> M <_ k )
22 5 21 syl 
 |-  ( ( ph /\ k e. A ) -> M <_ k )
23 zssre 
 |-  ZZ C_ RR
24 23 a1i 
 |-  ( ph -> ZZ C_ RR )
25 11 24 sstrd 
 |-  ( ph -> A C_ RR )
26 25 adantr 
 |-  ( ( ph /\ k e. A ) -> A C_ RR )
27 simpr 
 |-  ( ( ph /\ k e. A ) -> k e. A )
28 eqidd 
 |-  ( ( ph /\ k e. A ) -> sup ( A , RR , < ) = sup ( A , RR , < ) )
29 26 15 27 28 supfirege 
 |-  ( ( ph /\ k e. A ) -> k <_ sup ( A , RR , < ) )
30 20 22 29 jca32 
 |-  ( ( ph /\ k e. A ) -> ( ( M e. ZZ /\ sup ( A , RR , < ) e. ZZ /\ k e. ZZ ) /\ ( M <_ k /\ k <_ sup ( A , RR , < ) ) ) )
31 elfz2 
 |-  ( k e. ( M ... sup ( A , RR , < ) ) <-> ( ( M e. ZZ /\ sup ( A , RR , < ) e. ZZ /\ k e. ZZ ) /\ ( M <_ k /\ k <_ sup ( A , RR , < ) ) ) )
32 30 31 sylibr 
 |-  ( ( ph /\ k e. A ) -> k e. ( M ... sup ( A , RR , < ) ) )
33 32 ex 
 |-  ( ph -> ( k e. A -> k e. ( M ... sup ( A , RR , < ) ) ) )
34 33 ralrimiv 
 |-  ( ph -> A. k e. A k e. ( M ... sup ( A , RR , < ) ) )
35 dfss3 
 |-  ( A C_ ( M ... sup ( A , RR , < ) ) <-> A. k e. A k e. ( M ... sup ( A , RR , < ) ) )
36 34 35 sylibr 
 |-  ( ph -> A C_ ( M ... sup ( A , RR , < ) ) )