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 biimtrid 
 |-  ( ( ( 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 biimtrrid 
 |-  ( ( -. 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 ) ) )