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	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 ) )