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 ( 𝑠 < 𝑥 → 𝑥 ∉ 𝑆 ) ) )