Metamath Proof Explorer

Theorem ssnn0ssfz

Description: For any finite subset of NN0 , find a superset in the form of a set of sequential integers, analogous to ssnnssfz . (Contributed by AV, 30-Sep-2019)

Ref Expression
Assertion ssnn0ssfz 
|- ( A e. ( ~P NN0 i^i Fin ) -> E. n e. NN0 A C_ ( 0 ... n ) )

Proof

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