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 ( 𝑆 ⊆ ℕ0 → ( 𝑆 ∈ Fin ↔ ∃ 𝑠 ∈ ℕ0𝑥 ∈ ℕ0 ( 𝑠 < 𝑥𝑥𝑆 ) ) )

Proof

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