MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssnn0fi Structured version   Visualization version   GIF version

Theorem ssnn0fi 12974
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.)
Assertion
Ref Expression
ssnn0fi (𝑆 ⊆ ℕ0 → (𝑆 ∈ Fin ↔ ∃𝑠 ∈ ℕ0𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)))
Distinct variable group:   𝑆,𝑠,𝑥

Proof of Theorem ssnn0fi
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0nn0 11495 . . . . . 6 0 ∈ ℕ0
21a1i 11 . . . . 5 (𝑆 = ∅ → 0 ∈ ℕ0)
3 breq1 4803 . . . . . . . 8 (𝑠 = 0 → (𝑠 < 𝑥 ↔ 0 < 𝑥))
43imbi1d 330 . . . . . . 7 (𝑠 = 0 → ((𝑠 < 𝑥𝑥𝑆) ↔ (0 < 𝑥𝑥𝑆)))
54ralbidv 3120 . . . . . 6 (𝑠 = 0 → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆) ↔ ∀𝑥 ∈ ℕ0 (0 < 𝑥𝑥𝑆)))
65adantl 473 . . . . 5 ((𝑆 = ∅ ∧ 𝑠 = 0) → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆) ↔ ∀𝑥 ∈ ℕ0 (0 < 𝑥𝑥𝑆)))
7 nnel 3040 . . . . . . . . 9 𝑥𝑆𝑥𝑆)
8 n0i 4059 . . . . . . . . 9 (𝑥𝑆 → ¬ 𝑆 = ∅)
97, 8sylbi 207 . . . . . . . 8 𝑥𝑆 → ¬ 𝑆 = ∅)
109con4i 113 . . . . . . 7 (𝑆 = ∅ → 𝑥𝑆)
1110a1d 25 . . . . . 6 (𝑆 = ∅ → (0 < 𝑥𝑥𝑆))
1211ralrimivw 3101 . . . . 5 (𝑆 = ∅ → ∀𝑥 ∈ ℕ0 (0 < 𝑥𝑥𝑆))
132, 6, 12rspcedvd 3452 . . . 4 (𝑆 = ∅ → ∃𝑠 ∈ ℕ0𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆))
14132a1d 26 . . 3 (𝑆 = ∅ → (𝑆 ⊆ ℕ0 → (𝑆 ∈ Fin → ∃𝑠 ∈ ℕ0𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆))))
15 ltso 10306 . . . . . . 7 < Or ℝ
16 id 22 . . . . . . . . 9 (𝑆 ⊆ ℕ0𝑆 ⊆ ℕ0)
17 nn0ssre 11484 . . . . . . . . 9 0 ⊆ ℝ
1816, 17syl6ss 3752 . . . . . . . 8 (𝑆 ⊆ ℕ0𝑆 ⊆ ℝ)
19183anim3i 1158 . . . . . . 7 ((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0) → (𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℝ))
20 fisup2g 8535 . . . . . . 7 (( < Or ℝ ∧ (𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℝ)) → ∃𝑠𝑆 (∀𝑦𝑆 ¬ 𝑠 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑠 → ∃𝑧𝑆 𝑦 < 𝑧)))
2115, 19, 20sylancr 698 . . . . . 6 ((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0) → ∃𝑠𝑆 (∀𝑦𝑆 ¬ 𝑠 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑠 → ∃𝑧𝑆 𝑦 < 𝑧)))
22 simp3 1133 . . . . . . 7 ((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0) → 𝑆 ⊆ ℕ0)
23 breq2 4804 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → (𝑠 < 𝑦𝑠 < 𝑥))
2423notbid 307 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑥 → (¬ 𝑠 < 𝑦 ↔ ¬ 𝑠 < 𝑥))
2524rspcva 3443 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑆 ∧ ∀𝑦𝑆 ¬ 𝑠 < 𝑦) → ¬ 𝑠 < 𝑥)
26252a1d 26 . . . . . . . . . . . . . . . . 17 ((𝑥𝑆 ∧ ∀𝑦𝑆 ¬ 𝑠 < 𝑦) → (𝑥 ∈ ℕ0 → (((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0) ∧ 𝑠𝑆) → ¬ 𝑠 < 𝑥)))
2726expcom 450 . . . . . . . . . . . . . . . 16 (∀𝑦𝑆 ¬ 𝑠 < 𝑦 → (𝑥𝑆 → (𝑥 ∈ ℕ0 → (((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0) ∧ 𝑠𝑆) → ¬ 𝑠 < 𝑥))))
2827com24 95 . . . . . . . . . . . . . . 15 (∀𝑦𝑆 ¬ 𝑠 < 𝑦 → (((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0) ∧ 𝑠𝑆) → (𝑥 ∈ ℕ0 → (𝑥𝑆 → ¬ 𝑠 < 𝑥))))
2928imp31 447 . . . . . . . . . . . . . 14 (((∀𝑦𝑆 ¬ 𝑠 < 𝑦 ∧ ((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0) ∧ 𝑠𝑆)) ∧ 𝑥 ∈ ℕ0) → (𝑥𝑆 → ¬ 𝑠 < 𝑥))
307, 29syl5bi 232 . . . . . . . . . . . . 13 (((∀𝑦𝑆 ¬ 𝑠 < 𝑦 ∧ ((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0) ∧ 𝑠𝑆)) ∧ 𝑥 ∈ ℕ0) → (¬ 𝑥𝑆 → ¬ 𝑠 < 𝑥))
3130con4d 114 . . . . . . . . . . . 12 (((∀𝑦𝑆 ¬ 𝑠 < 𝑦 ∧ ((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0) ∧ 𝑠𝑆)) ∧ 𝑥 ∈ ℕ0) → (𝑠 < 𝑥𝑥𝑆))
3231ralrimiva 3100 . . . . . . . . . . 11 ((∀𝑦𝑆 ¬ 𝑠 < 𝑦 ∧ ((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0) ∧ 𝑠𝑆)) → ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆))
3332ex 449 . . . . . . . . . 10 (∀𝑦𝑆 ¬ 𝑠 < 𝑦 → (((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0) ∧ 𝑠𝑆) → ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)))
3433adantr 472 . . . . . . . . 9 ((∀𝑦𝑆 ¬ 𝑠 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑠 → ∃𝑧𝑆 𝑦 < 𝑧)) → (((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0) ∧ 𝑠𝑆) → ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)))
3534com12 32 . . . . . . . 8 (((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0) ∧ 𝑠𝑆) → ((∀𝑦𝑆 ¬ 𝑠 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑠 → ∃𝑧𝑆 𝑦 < 𝑧)) → ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)))
3635reximdva 3151 . . . . . . 7 ((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0) → (∃𝑠𝑆 (∀𝑦𝑆 ¬ 𝑠 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑠 → ∃𝑧𝑆 𝑦 < 𝑧)) → ∃𝑠𝑆𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)))
37 ssrexv 3804 . . . . . . 7 (𝑆 ⊆ ℕ0 → (∃𝑠𝑆𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆) → ∃𝑠 ∈ ℕ0𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)))
3822, 36, 37sylsyld 61 . . . . . 6 ((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0) → (∃𝑠𝑆 (∀𝑦𝑆 ¬ 𝑠 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑠 → ∃𝑧𝑆 𝑦 < 𝑧)) → ∃𝑠 ∈ ℕ0𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)))
3921, 38mpd 15 . . . . 5 ((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0) → ∃𝑠 ∈ ℕ0𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆))
40393exp 1113 . . . 4 (𝑆 ∈ Fin → (𝑆 ≠ ∅ → (𝑆 ⊆ ℕ0 → ∃𝑠 ∈ ℕ0𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆))))
4140com3l 89 . . 3 (𝑆 ≠ ∅ → (𝑆 ⊆ ℕ0 → (𝑆 ∈ Fin → ∃𝑠 ∈ ℕ0𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆))))
4214, 41pm2.61ine 3011 . 2 (𝑆 ⊆ ℕ0 → (𝑆 ∈ Fin → ∃𝑠 ∈ ℕ0𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)))
43 fzfi 12961 . . . . 5 (0...𝑠) ∈ Fin
44 elfz2nn0 12620 . . . . . . . . . . 11 (𝑦 ∈ (0...𝑠) ↔ (𝑦 ∈ ℕ0𝑠 ∈ ℕ0𝑦𝑠))
4544notbii 309 . . . . . . . . . 10 𝑦 ∈ (0...𝑠) ↔ ¬ (𝑦 ∈ ℕ0𝑠 ∈ ℕ0𝑦𝑠))
46 3ianor 1097 . . . . . . . . . 10 (¬ (𝑦 ∈ ℕ0𝑠 ∈ ℕ0𝑦𝑠) ↔ (¬ 𝑦 ∈ ℕ0 ∨ ¬ 𝑠 ∈ ℕ0 ∨ ¬ 𝑦𝑠))
47 3orass 1075 . . . . . . . . . 10 ((¬ 𝑦 ∈ ℕ0 ∨ ¬ 𝑠 ∈ ℕ0 ∨ ¬ 𝑦𝑠) ↔ (¬ 𝑦 ∈ ℕ0 ∨ (¬ 𝑠 ∈ ℕ0 ∨ ¬ 𝑦𝑠)))
4845, 46, 473bitri 286 . . . . . . . . 9 𝑦 ∈ (0...𝑠) ↔ (¬ 𝑦 ∈ ℕ0 ∨ (¬ 𝑠 ∈ ℕ0 ∨ ¬ 𝑦𝑠)))
49 ssel 3734 . . . . . . . . . . . . 13 (𝑆 ⊆ ℕ0 → (𝑦𝑆𝑦 ∈ ℕ0))
5049adantr 472 . . . . . . . . . . . 12 ((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) → (𝑦𝑆𝑦 ∈ ℕ0))
5150adantr 472 . . . . . . . . . . 11 (((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)) → (𝑦𝑆𝑦 ∈ ℕ0))
5251con3rr3 151 . . . . . . . . . 10 𝑦 ∈ ℕ0 → (((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)) → ¬ 𝑦𝑆))
53 notnotb 304 . . . . . . . . . . . 12 (𝑦 ∈ ℕ0 ↔ ¬ ¬ 𝑦 ∈ ℕ0)
54 pm2.24 121 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ℕ0 → (¬ 𝑠 ∈ ℕ0 → ¬ 𝑦𝑆))
5554adantl 473 . . . . . . . . . . . . . . . 16 ((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) → (¬ 𝑠 ∈ ℕ0 → ¬ 𝑦𝑆))
5655adantr 472 . . . . . . . . . . . . . . 15 (((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)) → (¬ 𝑠 ∈ ℕ0 → ¬ 𝑦𝑆))
5756com12 32 . . . . . . . . . . . . . 14 𝑠 ∈ ℕ0 → (((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)) → ¬ 𝑦𝑆))
5857a1d 25 . . . . . . . . . . . . 13 𝑠 ∈ ℕ0 → (𝑦 ∈ ℕ0 → (((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)) → ¬ 𝑦𝑆)))
59 breq2 4804 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝑠 < 𝑥𝑠 < 𝑦))
60 neleq1 3036 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝑥𝑆𝑦𝑆))
6159, 60imbi12d 333 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → ((𝑠 < 𝑥𝑥𝑆) ↔ (𝑠 < 𝑦𝑦𝑆)))
6261rspcva 3443 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)) → (𝑠 < 𝑦𝑦𝑆))
63 nn0re 11489 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ℕ0𝑠 ∈ ℝ)
64 nn0re 11489 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ℕ0𝑦 ∈ ℝ)
65 ltnle 10305 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑠 < 𝑦 ↔ ¬ 𝑦𝑠))
6663, 64, 65syl2an 495 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ ℕ0𝑦 ∈ ℕ0) → (𝑠 < 𝑦 ↔ ¬ 𝑦𝑠))
67 df-nel 3032 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦𝑆 ↔ ¬ 𝑦𝑆)
6867a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ ℕ0𝑦 ∈ ℕ0) → (𝑦𝑆 ↔ ¬ 𝑦𝑆))
6966, 68imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ ℕ0𝑦 ∈ ℕ0) → ((𝑠 < 𝑦𝑦𝑆) ↔ (¬ 𝑦𝑠 → ¬ 𝑦𝑆)))
7069biimpd 219 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 ∈ ℕ0𝑦 ∈ ℕ0) → ((𝑠 < 𝑦𝑦𝑆) → (¬ 𝑦𝑠 → ¬ 𝑦𝑆)))
7170ex 449 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ℕ0 → (𝑦 ∈ ℕ0 → ((𝑠 < 𝑦𝑦𝑆) → (¬ 𝑦𝑠 → ¬ 𝑦𝑆))))
7271adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) → (𝑦 ∈ ℕ0 → ((𝑠 < 𝑦𝑦𝑆) → (¬ 𝑦𝑠 → ¬ 𝑦𝑆))))
7372com12 32 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℕ0 → ((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) → ((𝑠 < 𝑦𝑦𝑆) → (¬ 𝑦𝑠 → ¬ 𝑦𝑆))))
7473adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)) → ((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) → ((𝑠 < 𝑦𝑦𝑆) → (¬ 𝑦𝑠 → ¬ 𝑦𝑆))))
7562, 74mpid 44 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)) → ((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) → (¬ 𝑦𝑠 → ¬ 𝑦𝑆)))
7675ex 449 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ0 → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆) → ((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) → (¬ 𝑦𝑠 → ¬ 𝑦𝑆))))
7776com13 88 . . . . . . . . . . . . . . 15 ((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆) → (𝑦 ∈ ℕ0 → (¬ 𝑦𝑠 → ¬ 𝑦𝑆))))
7877imp 444 . . . . . . . . . . . . . 14 (((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)) → (𝑦 ∈ ℕ0 → (¬ 𝑦𝑠 → ¬ 𝑦𝑆)))
7978com13 88 . . . . . . . . . . . . 13 𝑦𝑠 → (𝑦 ∈ ℕ0 → (((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)) → ¬ 𝑦𝑆)))
8058, 79jaoi 393 . . . . . . . . . . . 12 ((¬ 𝑠 ∈ ℕ0 ∨ ¬ 𝑦𝑠) → (𝑦 ∈ ℕ0 → (((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)) → ¬ 𝑦𝑆)))
8153, 80syl5bir 233 . . . . . . . . . . 11 ((¬ 𝑠 ∈ ℕ0 ∨ ¬ 𝑦𝑠) → (¬ ¬ 𝑦 ∈ ℕ0 → (((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)) → ¬ 𝑦𝑆)))
8281impcom 445 . . . . . . . . . 10 ((¬ ¬ 𝑦 ∈ ℕ0 ∧ (¬ 𝑠 ∈ ℕ0 ∨ ¬ 𝑦𝑠)) → (((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)) → ¬ 𝑦𝑆))
8352, 82jaoi3 1049 . . . . . . . . 9 ((¬ 𝑦 ∈ ℕ0 ∨ (¬ 𝑠 ∈ ℕ0 ∨ ¬ 𝑦𝑠)) → (((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)) → ¬ 𝑦𝑆))
8448, 83sylbi 207 . . . . . . . 8 𝑦 ∈ (0...𝑠) → (((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)) → ¬ 𝑦𝑆))
8584com12 32 . . . . . . 7 (((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)) → (¬ 𝑦 ∈ (0...𝑠) → ¬ 𝑦𝑆))
8685con4d 114 . . . . . 6 (((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)) → (𝑦𝑆𝑦 ∈ (0...𝑠)))
8786ssrdv 3746 . . . . 5 (((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)) → 𝑆 ⊆ (0...𝑠))
88 ssfi 8341 . . . . 5 (((0...𝑠) ∈ Fin ∧ 𝑆 ⊆ (0...𝑠)) → 𝑆 ∈ Fin)
8943, 87, 88sylancr 698 . . . 4 (((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)) → 𝑆 ∈ Fin)
9089ex 449 . . 3 ((𝑆 ⊆ ℕ0𝑠 ∈ ℕ0) → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆) → 𝑆 ∈ Fin))
9190rexlimdva 3165 . 2 (𝑆 ⊆ ℕ0 → (∃𝑠 ∈ ℕ0𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆) → 𝑆 ∈ Fin))
9242, 91impbid 202 1 (𝑆 ⊆ ℕ0 → (𝑆 ∈ Fin ↔ ∃𝑠 ∈ ℕ0𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥𝑆)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3o 1071  w3a 1072   = wceq 1628  wcel 2135  wne 2928  wnel 3031  wral 3046  wrex 3047  wss 3711  c0 4054   class class class wbr 4800   Or wor 5182  (class class class)co 6809  Fincfn 8117  cr 10123  0cc0 10124   < clt 10262  cle 10263  0cn0 11480  ...cfz 12515
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110  ax-cnex 10180  ax-resscn 10181  ax-1cn 10182  ax-icn 10183  ax-addcl 10184  ax-addrcl 10185  ax-mulcl 10186  ax-mulrcl 10187  ax-mulcom 10188  ax-addass 10189  ax-mulass 10190  ax-distr 10191  ax-i2m1 10192  ax-1ne0 10193  ax-1rid 10194  ax-rnegex 10195  ax-rrecex 10196  ax-cnre 10197  ax-pre-lttri 10198  ax-pre-lttrn 10199  ax-pre-ltadd 10200  ax-pre-mulgt0 10201
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-nel 3032  df-ral 3051  df-rex 3052  df-reu 3053  df-rmo 3054  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-pss 3727  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4585  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-tr 4901  df-id 5170  df-eprel 5175  df-po 5183  df-so 5184  df-fr 5221  df-we 5223  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-pred 5837  df-ord 5883  df-on 5884  df-lim 5885  df-suc 5886  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-riota 6770  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-om 7227  df-1st 7329  df-2nd 7330  df-wrecs 7572  df-recs 7633  df-rdg 7671  df-1o 7725  df-er 7907  df-en 8118  df-dom 8119  df-sdom 8120  df-fin 8121  df-pnf 10264  df-mnf 10265  df-xr 10266  df-ltxr 10267  df-le 10268  df-sub 10456  df-neg 10457  df-nn 11209  df-n0 11481  df-z 11566  df-uz 11876  df-fz 12516
This theorem is referenced by:  rabssnn0fi  12975
  Copyright terms: Public domain W3C validator