Metamath Proof Explorer


Theorem ssnn0fi

Description: A subset of the nonnegative integers is finite if and only if there is a nonnegative integer so that all integers greater than this integer are not contained in the subset. (Contributed by AV, 3-Oct-2019)

Ref Expression
Assertion ssnn0fi
|- ( S C_ NN0 -> ( S e. Fin <-> E. s e. NN0 A. x e. NN0 ( s < x -> x e/ S ) ) )

Proof

Step Hyp Ref Expression
1 0nn0
 |-  0 e. NN0
2 1 a1i
 |-  ( S = (/) -> 0 e. NN0 )
3 breq1
 |-  ( s = 0 -> ( s < x <-> 0 < x ) )
4 3 imbi1d
 |-  ( s = 0 -> ( ( s < x -> x e/ S ) <-> ( 0 < x -> x e/ S ) ) )
5 4 ralbidv
 |-  ( s = 0 -> ( A. x e. NN0 ( s < x -> x e/ S ) <-> A. x e. NN0 ( 0 < x -> x e/ S ) ) )
6 5 adantl
 |-  ( ( S = (/) /\ s = 0 ) -> ( A. x e. NN0 ( s < x -> x e/ S ) <-> A. x e. NN0 ( 0 < x -> x e/ S ) ) )
7 nnel
 |-  ( -. x e/ S <-> x e. S )
8 n0i
 |-  ( x e. S -> -. S = (/) )
9 7 8 sylbi
 |-  ( -. x e/ S -> -. S = (/) )
10 9 con4i
 |-  ( S = (/) -> x e/ S )
11 10 a1d
 |-  ( S = (/) -> ( 0 < x -> x e/ S ) )
12 11 ralrimivw
 |-  ( S = (/) -> A. x e. NN0 ( 0 < x -> x e/ S ) )
13 2 6 12 rspcedvd
 |-  ( S = (/) -> E. s e. NN0 A. x e. NN0 ( s < x -> x e/ S ) )
14 13 2a1d
 |-  ( S = (/) -> ( S C_ NN0 -> ( S e. Fin -> E. s e. NN0 A. x e. NN0 ( s < x -> x e/ S ) ) ) )
15 ltso
 |-  < Or RR
16 id
 |-  ( S C_ NN0 -> S C_ NN0 )
17 nn0ssre
 |-  NN0 C_ RR
18 16 17 sstrdi
 |-  ( S C_ NN0 -> S C_ RR )
19 18 3anim3i
 |-  ( ( S e. Fin /\ S =/= (/) /\ S C_ NN0 ) -> ( S e. Fin /\ S =/= (/) /\ S C_ RR ) )
20 fisup2g
 |-  ( ( < Or RR /\ ( S e. Fin /\ S =/= (/) /\ S C_ RR ) ) -> E. s e. S ( A. y e. S -. s < y /\ A. y e. RR ( y < s -> E. z e. S y < z ) ) )
21 15 19 20 sylancr
 |-  ( ( S e. Fin /\ S =/= (/) /\ S C_ NN0 ) -> E. s e. S ( A. y e. S -. s < y /\ A. y e. RR ( y < s -> E. z e. S y < z ) ) )
22 simp3
 |-  ( ( S e. Fin /\ S =/= (/) /\ S C_ NN0 ) -> S C_ NN0 )
23 breq2
 |-  ( y = x -> ( s < y <-> s < x ) )
24 23 notbid
 |-  ( y = x -> ( -. s < y <-> -. s < x ) )
25 24 rspcva
 |-  ( ( x e. S /\ A. y e. S -. s < y ) -> -. s < x )
26 25 2a1d
 |-  ( ( x e. S /\ A. y e. S -. s < y ) -> ( x e. NN0 -> ( ( ( S e. Fin /\ S =/= (/) /\ S C_ NN0 ) /\ s e. S ) -> -. s < x ) ) )
27 26 expcom
 |-  ( A. y e. S -. s < y -> ( x e. S -> ( x e. NN0 -> ( ( ( S e. Fin /\ S =/= (/) /\ S C_ NN0 ) /\ s e. S ) -> -. s < x ) ) ) )
28 27 com24
 |-  ( A. y e. S -. s < y -> ( ( ( S e. Fin /\ S =/= (/) /\ S C_ NN0 ) /\ s e. S ) -> ( x e. NN0 -> ( x e. S -> -. s < x ) ) ) )
29 28 imp31
 |-  ( ( ( A. y e. S -. s < y /\ ( ( S e. Fin /\ S =/= (/) /\ S C_ NN0 ) /\ s e. S ) ) /\ x e. NN0 ) -> ( x e. S -> -. s < x ) )
30 7 29 syl5bi
 |-  ( ( ( A. y e. S -. s < y /\ ( ( S e. Fin /\ S =/= (/) /\ S C_ NN0 ) /\ s e. S ) ) /\ x e. NN0 ) -> ( -. x e/ S -> -. s < x ) )
31 30 con4d
 |-  ( ( ( A. y e. S -. s < y /\ ( ( S e. Fin /\ S =/= (/) /\ S C_ NN0 ) /\ s e. S ) ) /\ x e. NN0 ) -> ( s < x -> x e/ S ) )
32 31 ralrimiva
 |-  ( ( A. y e. S -. s < y /\ ( ( S e. Fin /\ S =/= (/) /\ S C_ NN0 ) /\ s e. S ) ) -> A. x e. NN0 ( s < x -> x e/ S ) )
33 32 ex
 |-  ( A. y e. S -. s < y -> ( ( ( S e. Fin /\ S =/= (/) /\ S C_ NN0 ) /\ s e. S ) -> A. x e. NN0 ( s < x -> x e/ S ) ) )
34 33 adantr
 |-  ( ( A. y e. S -. s < y /\ A. y e. RR ( y < s -> E. z e. S y < z ) ) -> ( ( ( S e. Fin /\ S =/= (/) /\ S C_ NN0 ) /\ s e. S ) -> A. x e. NN0 ( s < x -> x e/ S ) ) )
35 34 com12
 |-  ( ( ( S e. Fin /\ S =/= (/) /\ S C_ NN0 ) /\ s e. S ) -> ( ( A. y e. S -. s < y /\ A. y e. RR ( y < s -> E. z e. S y < z ) ) -> A. x e. NN0 ( s < x -> x e/ S ) ) )
36 35 reximdva
 |-  ( ( S e. Fin /\ S =/= (/) /\ S C_ NN0 ) -> ( E. s e. S ( A. y e. S -. s < y /\ A. y e. RR ( y < s -> E. z e. S y < z ) ) -> E. s e. S A. x e. NN0 ( s < x -> x e/ S ) ) )
37 ssrexv
 |-  ( S C_ NN0 -> ( E. s e. S A. x e. NN0 ( s < x -> x e/ S ) -> E. s e. NN0 A. x e. NN0 ( s < x -> x e/ S ) ) )
38 22 36 37 sylsyld
 |-  ( ( S e. Fin /\ S =/= (/) /\ S C_ NN0 ) -> ( E. s e. S ( A. y e. S -. s < y /\ A. y e. RR ( y < s -> E. z e. S y < z ) ) -> E. s e. NN0 A. x e. NN0 ( s < x -> x e/ S ) ) )
39 21 38 mpd
 |-  ( ( S e. Fin /\ S =/= (/) /\ S C_ NN0 ) -> E. s e. NN0 A. x e. NN0 ( s < x -> x e/ S ) )
40 39 3exp
 |-  ( S e. Fin -> ( S =/= (/) -> ( S C_ NN0 -> E. s e. NN0 A. x e. NN0 ( s < x -> x e/ S ) ) ) )
41 40 com3l
 |-  ( S =/= (/) -> ( S C_ NN0 -> ( S e. Fin -> E. s e. NN0 A. x e. NN0 ( s < x -> x e/ S ) ) ) )
42 14 41 pm2.61ine
 |-  ( S C_ NN0 -> ( S e. Fin -> E. s e. NN0 A. x e. NN0 ( s < x -> x e/ S ) ) )
43 fzfi
 |-  ( 0 ... s ) e. Fin
44 elfz2nn0
 |-  ( y e. ( 0 ... s ) <-> ( y e. NN0 /\ s e. NN0 /\ y <_ s ) )
45 44 notbii
 |-  ( -. y e. ( 0 ... s ) <-> -. ( y e. NN0 /\ s e. NN0 /\ y <_ s ) )
46 3ianor
 |-  ( -. ( y e. NN0 /\ s e. NN0 /\ y <_ s ) <-> ( -. y e. NN0 \/ -. s e. NN0 \/ -. y <_ s ) )
47 3orass
 |-  ( ( -. y e. NN0 \/ -. s e. NN0 \/ -. y <_ s ) <-> ( -. y e. NN0 \/ ( -. s e. NN0 \/ -. y <_ s ) ) )
48 45 46 47 3bitri
 |-  ( -. y e. ( 0 ... s ) <-> ( -. y e. NN0 \/ ( -. s e. NN0 \/ -. y <_ s ) ) )
49 ssel
 |-  ( S C_ NN0 -> ( y e. S -> y e. NN0 ) )
50 49 adantr
 |-  ( ( S C_ NN0 /\ s e. NN0 ) -> ( y e. S -> y e. NN0 ) )
51 50 adantr
 |-  ( ( ( S C_ NN0 /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> x e/ S ) ) -> ( y e. S -> y e. NN0 ) )
52 51 con3rr3
 |-  ( -. y e. NN0 -> ( ( ( S C_ NN0 /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> x e/ S ) ) -> -. y e. S ) )
53 notnotb
 |-  ( y e. NN0 <-> -. -. y e. NN0 )
54 pm2.24
 |-  ( s e. NN0 -> ( -. s e. NN0 -> -. y e. S ) )
55 54 adantl
 |-  ( ( S C_ NN0 /\ s e. NN0 ) -> ( -. s e. NN0 -> -. y e. S ) )
56 55 adantr
 |-  ( ( ( S C_ NN0 /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> x e/ S ) ) -> ( -. s e. NN0 -> -. y e. S ) )
57 56 com12
 |-  ( -. s e. NN0 -> ( ( ( S C_ NN0 /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> x e/ S ) ) -> -. y e. S ) )
58 57 a1d
 |-  ( -. s e. NN0 -> ( y e. NN0 -> ( ( ( S C_ NN0 /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> x e/ S ) ) -> -. y e. S ) ) )
59 breq2
 |-  ( x = y -> ( s < x <-> s < y ) )
60 neleq1
 |-  ( x = y -> ( x e/ S <-> y e/ S ) )
61 59 60 imbi12d
 |-  ( x = y -> ( ( s < x -> x e/ S ) <-> ( s < y -> y e/ S ) ) )
62 61 rspcva
 |-  ( ( y e. NN0 /\ A. x e. NN0 ( s < x -> x e/ S ) ) -> ( s < y -> y e/ S ) )
63 nn0re
 |-  ( s e. NN0 -> s e. RR )
64 nn0re
 |-  ( y e. NN0 -> y e. RR )
65 ltnle
 |-  ( ( s e. RR /\ y e. RR ) -> ( s < y <-> -. y <_ s ) )
66 63 64 65 syl2an
 |-  ( ( s e. NN0 /\ y e. NN0 ) -> ( s < y <-> -. y <_ s ) )
67 df-nel
 |-  ( y e/ S <-> -. y e. S )
68 67 a1i
 |-  ( ( s e. NN0 /\ y e. NN0 ) -> ( y e/ S <-> -. y e. S ) )
69 66 68 imbi12d
 |-  ( ( s e. NN0 /\ y e. NN0 ) -> ( ( s < y -> y e/ S ) <-> ( -. y <_ s -> -. y e. S ) ) )
70 69 biimpd
 |-  ( ( s e. NN0 /\ y e. NN0 ) -> ( ( s < y -> y e/ S ) -> ( -. y <_ s -> -. y e. S ) ) )
71 70 ex
 |-  ( s e. NN0 -> ( y e. NN0 -> ( ( s < y -> y e/ S ) -> ( -. y <_ s -> -. y e. S ) ) ) )
72 71 adantl
 |-  ( ( S C_ NN0 /\ s e. NN0 ) -> ( y e. NN0 -> ( ( s < y -> y e/ S ) -> ( -. y <_ s -> -. y e. S ) ) ) )
73 72 com12
 |-  ( y e. NN0 -> ( ( S C_ NN0 /\ s e. NN0 ) -> ( ( s < y -> y e/ S ) -> ( -. y <_ s -> -. y e. S ) ) ) )
74 73 adantr
 |-  ( ( y e. NN0 /\ A. x e. NN0 ( s < x -> x e/ S ) ) -> ( ( S C_ NN0 /\ s e. NN0 ) -> ( ( s < y -> y e/ S ) -> ( -. y <_ s -> -. y e. S ) ) ) )
75 62 74 mpid
 |-  ( ( y e. NN0 /\ A. x e. NN0 ( s < x -> x e/ S ) ) -> ( ( S C_ NN0 /\ s e. NN0 ) -> ( -. y <_ s -> -. y e. S ) ) )
76 75 ex
 |-  ( y e. NN0 -> ( A. x e. NN0 ( s < x -> x e/ S ) -> ( ( S C_ NN0 /\ s e. NN0 ) -> ( -. y <_ s -> -. y e. S ) ) ) )
77 76 com13
 |-  ( ( S C_ NN0 /\ s e. NN0 ) -> ( A. x e. NN0 ( s < x -> x e/ S ) -> ( y e. NN0 -> ( -. y <_ s -> -. y e. S ) ) ) )
78 77 imp
 |-  ( ( ( S C_ NN0 /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> x e/ S ) ) -> ( y e. NN0 -> ( -. y <_ s -> -. y e. S ) ) )
79 78 com13
 |-  ( -. y <_ s -> ( y e. NN0 -> ( ( ( S C_ NN0 /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> x e/ S ) ) -> -. y e. S ) ) )
80 58 79 jaoi
 |-  ( ( -. s e. NN0 \/ -. y <_ s ) -> ( y e. NN0 -> ( ( ( S C_ NN0 /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> x e/ S ) ) -> -. y e. S ) ) )
81 53 80 syl5bir
 |-  ( ( -. s e. NN0 \/ -. y <_ s ) -> ( -. -. y e. NN0 -> ( ( ( S C_ NN0 /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> x e/ S ) ) -> -. y e. S ) ) )
82 81 impcom
 |-  ( ( -. -. y e. NN0 /\ ( -. s e. NN0 \/ -. y <_ s ) ) -> ( ( ( S C_ NN0 /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> x e/ S ) ) -> -. y e. S ) )
83 52 82 jaoi3
 |-  ( ( -. y e. NN0 \/ ( -. s e. NN0 \/ -. y <_ s ) ) -> ( ( ( S C_ NN0 /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> x e/ S ) ) -> -. y e. S ) )
84 48 83 sylbi
 |-  ( -. y e. ( 0 ... s ) -> ( ( ( S C_ NN0 /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> x e/ S ) ) -> -. y e. S ) )
85 84 com12
 |-  ( ( ( S C_ NN0 /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> x e/ S ) ) -> ( -. y e. ( 0 ... s ) -> -. y e. S ) )
86 85 con4d
 |-  ( ( ( S C_ NN0 /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> x e/ S ) ) -> ( y e. S -> y e. ( 0 ... s ) ) )
87 86 ssrdv
 |-  ( ( ( S C_ NN0 /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> x e/ S ) ) -> S C_ ( 0 ... s ) )
88 ssfi
 |-  ( ( ( 0 ... s ) e. Fin /\ S C_ ( 0 ... s ) ) -> S e. Fin )
89 43 87 88 sylancr
 |-  ( ( ( S C_ NN0 /\ s e. NN0 ) /\ A. x e. NN0 ( s < x -> x e/ S ) ) -> S e. Fin )
90 89 rexlimdva2
 |-  ( S C_ NN0 -> ( E. s e. NN0 A. x e. NN0 ( s < x -> x e/ S ) -> S e. Fin ) )
91 42 90 impbid
 |-  ( S C_ NN0 -> ( S e. Fin <-> E. s e. NN0 A. x e. NN0 ( s < x -> x e/ S ) ) )