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 eluzle 
 |-  ( k e. ( ZZ>= ` M ) -> M <_ k )
21 5 20 syl 
 |-  ( ( ph /\ k e. A ) -> M <_ k )
22 zssre 
 |-  ZZ C_ RR
23 22 a1i 
 |-  ( ph -> ZZ C_ RR )
24 11 23 sstrd 
 |-  ( ph -> A C_ RR )
25 24 adantr 
 |-  ( ( ph /\ k e. A ) -> A C_ RR )
26 simpr 
 |-  ( ( ph /\ k e. A ) -> k e. A )
27 eqidd 
 |-  ( ( ph /\ k e. A ) -> sup ( A , RR , < ) = sup ( A , RR , < ) )
28 25 15 26 27 supfirege 
 |-  ( ( ph /\ k e. A ) -> k <_ sup ( A , RR , < ) )
29 7 18 19 21 28 elfzd 
 |-  ( ( ph /\ k e. A ) -> k e. ( M ... sup ( A , RR , < ) ) )
30 29 ex 
 |-  ( ph -> ( k e. A -> k e. ( M ... sup ( A , RR , < ) ) ) )
31 30 ralrimiv 
 |-  ( ph -> A. k e. A k e. ( M ... sup ( A , RR , < ) ) )
32 dfss3 
 |-  ( A C_ ( M ... sup ( A , RR , < ) ) <-> A. k e. A k e. ( M ... sup ( A , RR , < ) ) )
33 31 32 sylibr 
 |-  ( ph -> A C_ ( M ... sup ( A , RR , < ) ) )