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

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