Metamath Proof Explorer


Theorem ssnnssfz

Description: For any finite subset of NN , find a superset in the form of a set of sequential integers. (Contributed by Thierry Arnoux, 13-Sep-2017)

Ref Expression
Assertion ssnnssfz
|- ( A e. ( ~P NN i^i Fin ) -> E. n e. NN A C_ ( 1 ... n ) )

Proof

Step Hyp Ref Expression
1 1nn
 |-  1 e. NN
2 simpr
 |-  ( ( A e. ( ~P NN i^i Fin ) /\ A = (/) ) -> A = (/) )
3 0ss
 |-  (/) C_ ( 1 ... 1 )
4 2 3 eqsstrdi
 |-  ( ( A e. ( ~P NN i^i Fin ) /\ A = (/) ) -> A C_ ( 1 ... 1 ) )
5 oveq2
 |-  ( n = 1 -> ( 1 ... n ) = ( 1 ... 1 ) )
6 5 sseq2d
 |-  ( n = 1 -> ( A C_ ( 1 ... n ) <-> A C_ ( 1 ... 1 ) ) )
7 6 rspcev
 |-  ( ( 1 e. NN /\ A C_ ( 1 ... 1 ) ) -> E. n e. NN A C_ ( 1 ... n ) )
8 1 4 7 sylancr
 |-  ( ( A e. ( ~P NN i^i Fin ) /\ A = (/) ) -> E. n e. NN A C_ ( 1 ... n ) )
9 elin
 |-  ( A e. ( ~P NN i^i Fin ) <-> ( A e. ~P NN /\ A e. Fin ) )
10 9 simplbi
 |-  ( A e. ( ~P NN i^i Fin ) -> A e. ~P NN )
11 10 adantr
 |-  ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> A e. ~P NN )
12 11 elpwid
 |-  ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> A C_ NN )
13 nnssre
 |-  NN C_ RR
14 ltso
 |-  < Or RR
15 soss
 |-  ( NN C_ RR -> ( < Or RR -> < Or NN ) )
16 13 14 15 mp2
 |-  < Or NN
17 16 a1i
 |-  ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> < Or NN )
18 9 simprbi
 |-  ( A e. ( ~P NN i^i Fin ) -> A e. Fin )
19 18 adantr
 |-  ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> A e. Fin )
20 simpr
 |-  ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> A =/= (/) )
21 fisupcl
 |-  ( ( < Or NN /\ ( A e. Fin /\ A =/= (/) /\ A C_ NN ) ) -> sup ( A , NN , < ) e. A )
22 17 19 20 12 21 syl13anc
 |-  ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> sup ( A , NN , < ) e. A )
23 12 22 sseldd
 |-  ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> sup ( A , NN , < ) e. NN )
24 12 sselda
 |-  ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> x e. NN )
25 nnuz
 |-  NN = ( ZZ>= ` 1 )
26 24 25 eleqtrdi
 |-  ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> x e. ( ZZ>= ` 1 ) )
27 24 nnzd
 |-  ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> x e. ZZ )
28 12 adantr
 |-  ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> A C_ NN )
29 22 adantr
 |-  ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> sup ( A , NN , < ) e. A )
30 28 29 sseldd
 |-  ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> sup ( A , NN , < ) e. NN )
31 30 nnzd
 |-  ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> sup ( A , NN , < ) e. ZZ )
32 fisup2g
 |-  ( ( < Or NN /\ ( A e. Fin /\ A =/= (/) /\ A C_ NN ) ) -> E. x e. A ( A. y e. A -. x < y /\ A. y e. NN ( y < x -> E. z e. A y < z ) ) )
33 17 19 20 12 32 syl13anc
 |-  ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> E. x e. A ( A. y e. A -. x < y /\ A. y e. NN ( y < x -> E. z e. A y < z ) ) )
34 ssrexv
 |-  ( A C_ NN -> ( E. x e. A ( A. y e. A -. x < y /\ A. y e. NN ( y < x -> E. z e. A y < z ) ) -> E. x e. NN ( A. y e. A -. x < y /\ A. y e. NN ( y < x -> E. z e. A y < z ) ) ) )
35 12 33 34 sylc
 |-  ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> E. x e. NN ( A. y e. A -. x < y /\ A. y e. NN ( y < x -> E. z e. A y < z ) ) )
36 17 35 supub
 |-  ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> ( x e. A -> -. sup ( A , NN , < ) < x ) )
37 36 imp
 |-  ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> -. sup ( A , NN , < ) < x )
38 24 nnred
 |-  ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> x e. RR )
39 30 nnred
 |-  ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> sup ( A , NN , < ) e. RR )
40 38 39 lenltd
 |-  ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> ( x <_ sup ( A , NN , < ) <-> -. sup ( A , NN , < ) < x ) )
41 37 40 mpbird
 |-  ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> x <_ sup ( A , NN , < ) )
42 eluz2
 |-  ( sup ( A , NN , < ) e. ( ZZ>= ` x ) <-> ( x e. ZZ /\ sup ( A , NN , < ) e. ZZ /\ x <_ sup ( A , NN , < ) ) )
43 27 31 41 42 syl3anbrc
 |-  ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> sup ( A , NN , < ) e. ( ZZ>= ` x ) )
44 eluzfz
 |-  ( ( x e. ( ZZ>= ` 1 ) /\ sup ( A , NN , < ) e. ( ZZ>= ` x ) ) -> x e. ( 1 ... sup ( A , NN , < ) ) )
45 26 43 44 syl2anc
 |-  ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> x e. ( 1 ... sup ( A , NN , < ) ) )
46 45 ex
 |-  ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> ( x e. A -> x e. ( 1 ... sup ( A , NN , < ) ) ) )
47 46 ssrdv
 |-  ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> A C_ ( 1 ... sup ( A , NN , < ) ) )
48 oveq2
 |-  ( n = sup ( A , NN , < ) -> ( 1 ... n ) = ( 1 ... sup ( A , NN , < ) ) )
49 48 sseq2d
 |-  ( n = sup ( A , NN , < ) -> ( A C_ ( 1 ... n ) <-> A C_ ( 1 ... sup ( A , NN , < ) ) ) )
50 49 rspcev
 |-  ( ( sup ( A , NN , < ) e. NN /\ A C_ ( 1 ... sup ( A , NN , < ) ) ) -> E. n e. NN A C_ ( 1 ... n ) )
51 23 47 50 syl2anc
 |-  ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> E. n e. NN A C_ ( 1 ... n ) )
52 8 51 pm2.61dane
 |-  ( A e. ( ~P NN i^i Fin ) -> E. n e. NN A C_ ( 1 ... n ) )