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 0 S Fin s 0 x 0 s < x x S

Proof

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