Step | Hyp | Ref
| Expression |
1 | | 0nn0 11984 |
. . . . . 6
⊢ 0 ∈
ℕ0 |
2 | 1 | a1i 11 |
. . . . 5
⊢ (𝑆 = ∅ → 0 ∈
ℕ0) |
3 | | breq1 5030 |
. . . . . . . 8
⊢ (𝑠 = 0 → (𝑠 < 𝑥 ↔ 0 < 𝑥)) |
4 | 3 | imbi1d 345 |
. . . . . . 7
⊢ (𝑠 = 0 → ((𝑠 < 𝑥 → 𝑥 ∉ 𝑆) ↔ (0 < 𝑥 → 𝑥 ∉ 𝑆))) |
5 | 4 | ralbidv 3109 |
. . . . . 6
⊢ (𝑠 = 0 → (∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → 𝑥 ∉ 𝑆) ↔ ∀𝑥 ∈ ℕ0 (0 < 𝑥 → 𝑥 ∉ 𝑆))) |
6 | 5 | adantl 485 |
. . . . 5
⊢ ((𝑆 = ∅ ∧ 𝑠 = 0) → (∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → 𝑥 ∉ 𝑆) ↔ ∀𝑥 ∈ ℕ0 (0 < 𝑥 → 𝑥 ∉ 𝑆))) |
7 | | nnel 3047 |
. . . . . . . . 9
⊢ (¬
𝑥 ∉ 𝑆 ↔ 𝑥 ∈ 𝑆) |
8 | | n0i 4220 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑆 → ¬ 𝑆 = ∅) |
9 | 7, 8 | sylbi 220 |
. . . . . . . 8
⊢ (¬
𝑥 ∉ 𝑆 → ¬ 𝑆 = ∅) |
10 | 9 | con4i 114 |
. . . . . . 7
⊢ (𝑆 = ∅ → 𝑥 ∉ 𝑆) |
11 | 10 | a1d 25 |
. . . . . 6
⊢ (𝑆 = ∅ → (0 < 𝑥 → 𝑥 ∉ 𝑆)) |
12 | 11 | ralrimivw 3097 |
. . . . 5
⊢ (𝑆 = ∅ → ∀𝑥 ∈ ℕ0 (0
< 𝑥 → 𝑥 ∉ 𝑆)) |
13 | 2, 6, 12 | rspcedvd 3527 |
. . . 4
⊢ (𝑆 = ∅ → ∃𝑠 ∈ ℕ0
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → 𝑥 ∉ 𝑆)) |
14 | 13 | 2a1d 26 |
. . 3
⊢ (𝑆 = ∅ → (𝑆 ⊆ ℕ0
→ (𝑆 ∈ Fin →
∃𝑠 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆)))) |
15 | | ltso 10792 |
. . . . . . 7
⊢ < Or
ℝ |
16 | | id 22 |
. . . . . . . . 9
⊢ (𝑆 ⊆ ℕ0
→ 𝑆 ⊆
ℕ0) |
17 | | nn0ssre 11973 |
. . . . . . . . 9
⊢
ℕ0 ⊆ ℝ |
18 | 16, 17 | sstrdi 3887 |
. . . . . . . 8
⊢ (𝑆 ⊆ ℕ0
→ 𝑆 ⊆
ℝ) |
19 | 18 | 3anim3i 1155 |
. . . . . . 7
⊢ ((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0)
→ (𝑆 ∈ Fin ∧
𝑆 ≠ ∅ ∧ 𝑆 ⊆
ℝ)) |
20 | | fisup2g 8998 |
. . . . . . 7
⊢ (( <
Or ℝ ∧ (𝑆 ∈
Fin ∧ 𝑆 ≠ ∅
∧ 𝑆 ⊆ ℝ))
→ ∃𝑠 ∈
𝑆 (∀𝑦 ∈ 𝑆 ¬ 𝑠 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑠 → ∃𝑧 ∈ 𝑆 𝑦 < 𝑧))) |
21 | 15, 19, 20 | sylancr 590 |
. . . . . 6
⊢ ((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0)
→ ∃𝑠 ∈
𝑆 (∀𝑦 ∈ 𝑆 ¬ 𝑠 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑠 → ∃𝑧 ∈ 𝑆 𝑦 < 𝑧))) |
22 | | simp3 1139 |
. . . . . . 7
⊢ ((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0)
→ 𝑆 ⊆
ℕ0) |
23 | | breq2 5031 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑥 → (𝑠 < 𝑦 ↔ 𝑠 < 𝑥)) |
24 | 23 | notbid 321 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑥 → (¬ 𝑠 < 𝑦 ↔ ¬ 𝑠 < 𝑥)) |
25 | 24 | rspcva 3522 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 ¬ 𝑠 < 𝑦) → ¬ 𝑠 < 𝑥) |
26 | 25 | 2a1d 26 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 ¬ 𝑠 < 𝑦) → (𝑥 ∈ ℕ0 → (((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0)
∧ 𝑠 ∈ 𝑆) → ¬ 𝑠 < 𝑥))) |
27 | 26 | expcom 417 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑦 ∈
𝑆 ¬ 𝑠 < 𝑦 → (𝑥 ∈ 𝑆 → (𝑥 ∈ ℕ0 → (((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0)
∧ 𝑠 ∈ 𝑆) → ¬ 𝑠 < 𝑥)))) |
28 | 27 | com24 95 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑦 ∈
𝑆 ¬ 𝑠 < 𝑦 → (((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0) ∧ 𝑠 ∈ 𝑆) → (𝑥 ∈ ℕ0 → (𝑥 ∈ 𝑆 → ¬ 𝑠 < 𝑥)))) |
29 | 28 | imp31 421 |
. . . . . . . . . . . . . 14
⊢
(((∀𝑦 ∈
𝑆 ¬ 𝑠 < 𝑦 ∧ ((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0) ∧ 𝑠 ∈ 𝑆)) ∧ 𝑥 ∈ ℕ0) → (𝑥 ∈ 𝑆 → ¬ 𝑠 < 𝑥)) |
30 | 7, 29 | syl5bi 245 |
. . . . . . . . . . . . 13
⊢
(((∀𝑦 ∈
𝑆 ¬ 𝑠 < 𝑦 ∧ ((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0) ∧ 𝑠 ∈ 𝑆)) ∧ 𝑥 ∈ ℕ0) → (¬
𝑥 ∉ 𝑆 → ¬ 𝑠 < 𝑥)) |
31 | 30 | con4d 115 |
. . . . . . . . . . . 12
⊢
(((∀𝑦 ∈
𝑆 ¬ 𝑠 < 𝑦 ∧ ((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0) ∧ 𝑠 ∈ 𝑆)) ∧ 𝑥 ∈ ℕ0) → (𝑠 < 𝑥 → 𝑥 ∉ 𝑆)) |
32 | 31 | ralrimiva 3096 |
. . . . . . . . . . 11
⊢
((∀𝑦 ∈
𝑆 ¬ 𝑠 < 𝑦 ∧ ((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0) ∧ 𝑠 ∈ 𝑆)) → ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆)) |
33 | 32 | ex 416 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
𝑆 ¬ 𝑠 < 𝑦 → (((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0) ∧ 𝑠 ∈ 𝑆) → ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆))) |
34 | 33 | adantr 484 |
. . . . . . . . 9
⊢
((∀𝑦 ∈
𝑆 ¬ 𝑠 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑠 → ∃𝑧 ∈ 𝑆 𝑦 < 𝑧)) → (((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0) ∧ 𝑠 ∈ 𝑆) → ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆))) |
35 | 34 | com12 32 |
. . . . . . . 8
⊢ (((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0)
∧ 𝑠 ∈ 𝑆) → ((∀𝑦 ∈ 𝑆 ¬ 𝑠 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑠 → ∃𝑧 ∈ 𝑆 𝑦 < 𝑧)) → ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆))) |
36 | 35 | reximdva 3183 |
. . . . . . 7
⊢ ((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0)
→ (∃𝑠 ∈
𝑆 (∀𝑦 ∈ 𝑆 ¬ 𝑠 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑠 → ∃𝑧 ∈ 𝑆 𝑦 < 𝑧)) → ∃𝑠 ∈ 𝑆 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆))) |
37 | | ssrexv 3942 |
. . . . . . 7
⊢ (𝑆 ⊆ ℕ0
→ (∃𝑠 ∈
𝑆 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → 𝑥 ∉ 𝑆) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → 𝑥 ∉ 𝑆))) |
38 | 22, 36, 37 | sylsyld 61 |
. . . . . 6
⊢ ((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0)
→ (∃𝑠 ∈
𝑆 (∀𝑦 ∈ 𝑆 ¬ 𝑠 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑠 → ∃𝑧 ∈ 𝑆 𝑦 < 𝑧)) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → 𝑥 ∉ 𝑆))) |
39 | 21, 38 | mpd 15 |
. . . . 5
⊢ ((𝑆 ∈ Fin ∧ 𝑆 ≠ ∅ ∧ 𝑆 ⊆ ℕ0)
→ ∃𝑠 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆)) |
40 | 39 | 3exp 1120 |
. . . 4
⊢ (𝑆 ∈ Fin → (𝑆 ≠ ∅ → (𝑆 ⊆ ℕ0
→ ∃𝑠 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆)))) |
41 | 40 | com3l 89 |
. . 3
⊢ (𝑆 ≠ ∅ → (𝑆 ⊆ ℕ0
→ (𝑆 ∈ Fin →
∃𝑠 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆)))) |
42 | 14, 41 | pm2.61ine 3017 |
. 2
⊢ (𝑆 ⊆ ℕ0
→ (𝑆 ∈ Fin →
∃𝑠 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆))) |
43 | | fzfi 13424 |
. . . 4
⊢
(0...𝑠) ∈
Fin |
44 | | elfz2nn0 13082 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (0...𝑠) ↔ (𝑦 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0
∧ 𝑦 ≤ 𝑠)) |
45 | 44 | notbii 323 |
. . . . . . . . 9
⊢ (¬
𝑦 ∈ (0...𝑠) ↔ ¬ (𝑦 ∈ ℕ0
∧ 𝑠 ∈
ℕ0 ∧ 𝑦
≤ 𝑠)) |
46 | | 3ianor 1108 |
. . . . . . . . 9
⊢ (¬
(𝑦 ∈
ℕ0 ∧ 𝑠
∈ ℕ0 ∧ 𝑦 ≤ 𝑠) ↔ (¬ 𝑦 ∈ ℕ0 ∨ ¬ 𝑠 ∈ ℕ0 ∨
¬ 𝑦 ≤ 𝑠)) |
47 | | 3orass 1091 |
. . . . . . . . 9
⊢ ((¬
𝑦 ∈
ℕ0 ∨ ¬ 𝑠 ∈ ℕ0 ∨ ¬ 𝑦 ≤ 𝑠) ↔ (¬ 𝑦 ∈ ℕ0 ∨ (¬ 𝑠 ∈ ℕ0 ∨
¬ 𝑦 ≤ 𝑠))) |
48 | 45, 46, 47 | 3bitri 300 |
. . . . . . . 8
⊢ (¬
𝑦 ∈ (0...𝑠) ↔ (¬ 𝑦 ∈ ℕ0 ∨
(¬ 𝑠 ∈
ℕ0 ∨ ¬ 𝑦 ≤ 𝑠))) |
49 | | ssel 3868 |
. . . . . . . . . . . 12
⊢ (𝑆 ⊆ ℕ0
→ (𝑦 ∈ 𝑆 → 𝑦 ∈
ℕ0)) |
50 | 49 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑆 ⊆ ℕ0
∧ 𝑠 ∈
ℕ0) → (𝑦 ∈ 𝑆 → 𝑦 ∈
ℕ0)) |
51 | 50 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝑆 ⊆ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆)) → (𝑦 ∈ 𝑆 → 𝑦 ∈
ℕ0)) |
52 | 51 | con3rr3 158 |
. . . . . . . . 9
⊢ (¬
𝑦 ∈
ℕ0 → (((𝑆 ⊆ ℕ0 ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → 𝑥 ∉ 𝑆)) → ¬ 𝑦 ∈ 𝑆)) |
53 | | notnotb 318 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
↔ ¬ ¬ 𝑦 ∈
ℕ0) |
54 | | pm2.24 124 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ℕ0
→ (¬ 𝑠 ∈
ℕ0 → ¬ 𝑦 ∈ 𝑆)) |
55 | 54 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ⊆ ℕ0
∧ 𝑠 ∈
ℕ0) → (¬ 𝑠 ∈ ℕ0 → ¬
𝑦 ∈ 𝑆)) |
56 | 55 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ⊆ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆)) → (¬ 𝑠 ∈ ℕ0 → ¬
𝑦 ∈ 𝑆)) |
57 | 56 | com12 32 |
. . . . . . . . . . . . 13
⊢ (¬
𝑠 ∈
ℕ0 → (((𝑆 ⊆ ℕ0 ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → 𝑥 ∉ 𝑆)) → ¬ 𝑦 ∈ 𝑆)) |
58 | 57 | a1d 25 |
. . . . . . . . . . . 12
⊢ (¬
𝑠 ∈
ℕ0 → (𝑦 ∈ ℕ0 → (((𝑆 ⊆ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆)) → ¬ 𝑦 ∈ 𝑆))) |
59 | | breq2 5031 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → (𝑠 < 𝑥 ↔ 𝑠 < 𝑦)) |
60 | | neleq1 3043 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → (𝑥 ∉ 𝑆 ↔ 𝑦 ∉ 𝑆)) |
61 | 59, 60 | imbi12d 348 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ((𝑠 < 𝑥 → 𝑥 ∉ 𝑆) ↔ (𝑠 < 𝑦 → 𝑦 ∉ 𝑆))) |
62 | 61 | rspcva 3522 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → 𝑥 ∉ 𝑆)) → (𝑠 < 𝑦 → 𝑦 ∉ 𝑆)) |
63 | | nn0re 11978 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑠 ∈ ℕ0
→ 𝑠 ∈
ℝ) |
64 | | nn0re 11978 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℝ) |
65 | | ltnle 10791 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑠 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑠 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑠)) |
66 | 63, 64, 65 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑠 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → (𝑠 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑠)) |
67 | | df-nel 3039 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∉ 𝑆 ↔ ¬ 𝑦 ∈ 𝑆) |
68 | 67 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑠 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → (𝑦 ∉ 𝑆 ↔ ¬ 𝑦 ∈ 𝑆)) |
69 | 66, 68 | imbi12d 348 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑠 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → ((𝑠 < 𝑦 → 𝑦 ∉ 𝑆) ↔ (¬ 𝑦 ≤ 𝑠 → ¬ 𝑦 ∈ 𝑆))) |
70 | 69 | biimpd 232 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑠 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → ((𝑠 < 𝑦 → 𝑦 ∉ 𝑆) → (¬ 𝑦 ≤ 𝑠 → ¬ 𝑦 ∈ 𝑆))) |
71 | 70 | ex 416 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 ∈ ℕ0
→ (𝑦 ∈
ℕ0 → ((𝑠 < 𝑦 → 𝑦 ∉ 𝑆) → (¬ 𝑦 ≤ 𝑠 → ¬ 𝑦 ∈ 𝑆)))) |
72 | 71 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ⊆ ℕ0
∧ 𝑠 ∈
ℕ0) → (𝑦 ∈ ℕ0 → ((𝑠 < 𝑦 → 𝑦 ∉ 𝑆) → (¬ 𝑦 ≤ 𝑠 → ¬ 𝑦 ∈ 𝑆)))) |
73 | 72 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ0
→ ((𝑆 ⊆
ℕ0 ∧ 𝑠
∈ ℕ0) → ((𝑠 < 𝑦 → 𝑦 ∉ 𝑆) → (¬ 𝑦 ≤ 𝑠 → ¬ 𝑦 ∈ 𝑆)))) |
74 | 73 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → 𝑥 ∉ 𝑆)) → ((𝑆 ⊆ ℕ0 ∧ 𝑠 ∈ ℕ0)
→ ((𝑠 < 𝑦 → 𝑦 ∉ 𝑆) → (¬ 𝑦 ≤ 𝑠 → ¬ 𝑦 ∈ 𝑆)))) |
75 | 62, 74 | mpid 44 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → 𝑥 ∉ 𝑆)) → ((𝑆 ⊆ ℕ0 ∧ 𝑠 ∈ ℕ0)
→ (¬ 𝑦 ≤ 𝑠 → ¬ 𝑦 ∈ 𝑆))) |
76 | 75 | ex 416 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ0
→ (∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → 𝑥 ∉ 𝑆) → ((𝑆 ⊆ ℕ0 ∧ 𝑠 ∈ ℕ0)
→ (¬ 𝑦 ≤ 𝑠 → ¬ 𝑦 ∈ 𝑆)))) |
77 | 76 | com13 88 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ⊆ ℕ0
∧ 𝑠 ∈
ℕ0) → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆) → (𝑦 ∈ ℕ0 → (¬
𝑦 ≤ 𝑠 → ¬ 𝑦 ∈ 𝑆)))) |
78 | 77 | imp 410 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ⊆ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆)) → (𝑦 ∈ ℕ0 → (¬
𝑦 ≤ 𝑠 → ¬ 𝑦 ∈ 𝑆))) |
79 | 78 | com13 88 |
. . . . . . . . . . . 12
⊢ (¬
𝑦 ≤ 𝑠 → (𝑦 ∈ ℕ0 → (((𝑆 ⊆ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆)) → ¬ 𝑦 ∈ 𝑆))) |
80 | 58, 79 | jaoi 856 |
. . . . . . . . . . 11
⊢ ((¬
𝑠 ∈
ℕ0 ∨ ¬ 𝑦 ≤ 𝑠) → (𝑦 ∈ ℕ0 → (((𝑆 ⊆ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆)) → ¬ 𝑦 ∈ 𝑆))) |
81 | 53, 80 | syl5bir 246 |
. . . . . . . . . 10
⊢ ((¬
𝑠 ∈
ℕ0 ∨ ¬ 𝑦 ≤ 𝑠) → (¬ ¬ 𝑦 ∈ ℕ0 → (((𝑆 ⊆ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆)) → ¬ 𝑦 ∈ 𝑆))) |
82 | 81 | impcom 411 |
. . . . . . . . 9
⊢ ((¬
¬ 𝑦 ∈
ℕ0 ∧ (¬ 𝑠 ∈ ℕ0 ∨ ¬ 𝑦 ≤ 𝑠)) → (((𝑆 ⊆ ℕ0 ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → 𝑥 ∉ 𝑆)) → ¬ 𝑦 ∈ 𝑆)) |
83 | 52, 82 | jaoi3 1060 |
. . . . . . . 8
⊢ ((¬
𝑦 ∈
ℕ0 ∨ (¬ 𝑠 ∈ ℕ0 ∨ ¬ 𝑦 ≤ 𝑠)) → (((𝑆 ⊆ ℕ0 ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → 𝑥 ∉ 𝑆)) → ¬ 𝑦 ∈ 𝑆)) |
84 | 48, 83 | sylbi 220 |
. . . . . . 7
⊢ (¬
𝑦 ∈ (0...𝑠) → (((𝑆 ⊆ ℕ0 ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → 𝑥 ∉ 𝑆)) → ¬ 𝑦 ∈ 𝑆)) |
85 | 84 | com12 32 |
. . . . . 6
⊢ (((𝑆 ⊆ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆)) → (¬ 𝑦 ∈ (0...𝑠) → ¬ 𝑦 ∈ 𝑆)) |
86 | 85 | con4d 115 |
. . . . 5
⊢ (((𝑆 ⊆ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆)) → (𝑦 ∈ 𝑆 → 𝑦 ∈ (0...𝑠))) |
87 | 86 | ssrdv 3881 |
. . . 4
⊢ (((𝑆 ⊆ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆)) → 𝑆 ⊆ (0...𝑠)) |
88 | | ssfi 8765 |
. . . 4
⊢
(((0...𝑠) ∈ Fin
∧ 𝑆 ⊆ (0...𝑠)) → 𝑆 ∈ Fin) |
89 | 43, 87, 88 | sylancr 590 |
. . 3
⊢ (((𝑆 ⊆ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆)) → 𝑆 ∈ Fin) |
90 | 89 | rexlimdva2 3196 |
. 2
⊢ (𝑆 ⊆ ℕ0
→ (∃𝑠 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆) → 𝑆 ∈ Fin)) |
91 | 42, 90 | impbid 215 |
1
⊢ (𝑆 ⊆ ℕ0
→ (𝑆 ∈ Fin ↔
∃𝑠 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆))) |