Step | Hyp | Ref
| Expression |
1 | | nfra1 3144 |
. . . 4
⊢
Ⅎ𝑛∀𝑛 ∈ ω 𝑛 ≼ 𝐴 |
2 | | breq1 5077 |
. . . . . . 7
⊢ (𝑦 = 𝑛 → (𝑦 ≺ 𝐴 ↔ 𝑛 ≺ 𝐴)) |
3 | 2 | imbi2d 341 |
. . . . . 6
⊢ (𝑦 = 𝑛 → ((∀𝑛 ∈ ω 𝑛 ≼ 𝐴 → 𝑦 ≺ 𝐴) ↔ (∀𝑛 ∈ ω 𝑛 ≼ 𝐴 → 𝑛 ≺ 𝐴))) |
4 | | breq1 5077 |
. . . . . . 7
⊢ (𝑦 = ∅ → (𝑦 ≺ 𝐴 ↔ ∅ ≺ 𝐴)) |
5 | | breq1 5077 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → (𝑦 ≺ 𝐴 ↔ 𝑧 ≺ 𝐴)) |
6 | | breq1 5077 |
. . . . . . 7
⊢ (𝑦 = suc 𝑧 → (𝑦 ≺ 𝐴 ↔ suc 𝑧 ≺ 𝐴)) |
7 | | 1n0 8318 |
. . . . . . . . 9
⊢
1o ≠ ∅ |
8 | | 1onn 8470 |
. . . . . . . . . 10
⊢
1o ∈ ω |
9 | | 0sdomg 8891 |
. . . . . . . . . 10
⊢
(1o ∈ ω → (∅ ≺ 1o
↔ 1o ≠ ∅)) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . 9
⊢ (∅
≺ 1o ↔ 1o ≠ ∅) |
11 | 7, 10 | mpbir 230 |
. . . . . . . 8
⊢ ∅
≺ 1o |
12 | | breq1 5077 |
. . . . . . . . . 10
⊢ (𝑛 = 1o → (𝑛 ≼ 𝐴 ↔ 1o ≼ 𝐴)) |
13 | 12 | rspccv 3558 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
ω 𝑛 ≼ 𝐴 → (1o ∈
ω → 1o ≼ 𝐴)) |
14 | 8, 13 | mpi 20 |
. . . . . . . 8
⊢
(∀𝑛 ∈
ω 𝑛 ≼ 𝐴 → 1o ≼
𝐴) |
15 | | sdomdomtr 8897 |
. . . . . . . 8
⊢ ((∅
≺ 1o ∧ 1o ≼ 𝐴) → ∅ ≺ 𝐴) |
16 | 11, 14, 15 | sylancr 587 |
. . . . . . 7
⊢
(∀𝑛 ∈
ω 𝑛 ≼ 𝐴 → ∅ ≺ 𝐴) |
17 | | peano2 7737 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ω → suc 𝑧 ∈
ω) |
18 | | php4 8996 |
. . . . . . . . . . 11
⊢ (suc
𝑧 ∈ ω → suc
𝑧 ≺ suc suc 𝑧) |
19 | 17, 18 | syl 17 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ω → suc 𝑧 ≺ suc suc 𝑧) |
20 | | breq1 5077 |
. . . . . . . . . . . 12
⊢ (𝑛 = suc suc 𝑧 → (𝑛 ≼ 𝐴 ↔ suc suc 𝑧 ≼ 𝐴)) |
21 | 20 | rspccv 3558 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
ω 𝑛 ≼ 𝐴 → (suc suc 𝑧 ∈ ω → suc suc
𝑧 ≼ 𝐴)) |
22 | | peano2 7737 |
. . . . . . . . . . . 12
⊢ (suc
𝑧 ∈ ω → suc
suc 𝑧 ∈
ω) |
23 | 17, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ω → suc suc
𝑧 ∈
ω) |
24 | 21, 23 | impel 506 |
. . . . . . . . . 10
⊢
((∀𝑛 ∈
ω 𝑛 ≼ 𝐴 ∧ 𝑧 ∈ ω) → suc suc 𝑧 ≼ 𝐴) |
25 | | sdomdomtr 8897 |
. . . . . . . . . 10
⊢ ((suc
𝑧 ≺ suc suc 𝑧 ∧ suc suc 𝑧 ≼ 𝐴) → suc 𝑧 ≺ 𝐴) |
26 | 19, 24, 25 | syl2an2 683 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
ω 𝑛 ≼ 𝐴 ∧ 𝑧 ∈ ω) → suc 𝑧 ≺ 𝐴) |
27 | 26 | a1d 25 |
. . . . . . . 8
⊢
((∀𝑛 ∈
ω 𝑛 ≼ 𝐴 ∧ 𝑧 ∈ ω) → (𝑧 ≺ 𝐴 → suc 𝑧 ≺ 𝐴)) |
28 | 27 | expcom 414 |
. . . . . . 7
⊢ (𝑧 ∈ ω →
(∀𝑛 ∈ ω
𝑛 ≼ 𝐴 → (𝑧 ≺ 𝐴 → suc 𝑧 ≺ 𝐴))) |
29 | 4, 5, 6, 16, 28 | finds2 7747 |
. . . . . 6
⊢ (𝑦 ∈ ω →
(∀𝑛 ∈ ω
𝑛 ≼ 𝐴 → 𝑦 ≺ 𝐴)) |
30 | 3, 29 | vtoclga 3513 |
. . . . 5
⊢ (𝑛 ∈ ω →
(∀𝑛 ∈ ω
𝑛 ≼ 𝐴 → 𝑛 ≺ 𝐴)) |
31 | 30 | com12 32 |
. . . 4
⊢
(∀𝑛 ∈
ω 𝑛 ≼ 𝐴 → (𝑛 ∈ ω → 𝑛 ≺ 𝐴)) |
32 | 1, 31 | ralrimi 3141 |
. . 3
⊢
(∀𝑛 ∈
ω 𝑛 ≼ 𝐴 → ∀𝑛 ∈ ω 𝑛 ≺ 𝐴) |
33 | | sdomnen 8769 |
. . . . 5
⊢ (𝑛 ≺ 𝐴 → ¬ 𝑛 ≈ 𝐴) |
34 | | ensym 8789 |
. . . . 5
⊢ (𝐴 ≈ 𝑛 → 𝑛 ≈ 𝐴) |
35 | 33, 34 | nsyl 140 |
. . . 4
⊢ (𝑛 ≺ 𝐴 → ¬ 𝐴 ≈ 𝑛) |
36 | 35 | ralimi 3087 |
. . 3
⊢
(∀𝑛 ∈
ω 𝑛 ≺ 𝐴 → ∀𝑛 ∈ ω ¬ 𝐴 ≈ 𝑛) |
37 | 32, 36 | syl 17 |
. 2
⊢
(∀𝑛 ∈
ω 𝑛 ≼ 𝐴 → ∀𝑛 ∈ ω ¬ 𝐴 ≈ 𝑛) |
38 | | isfi 8764 |
. . . 4
⊢ (𝐴 ∈ Fin ↔ ∃𝑛 ∈ ω 𝐴 ≈ 𝑛) |
39 | 38 | notbii 320 |
. . 3
⊢ (¬
𝐴 ∈ Fin ↔ ¬
∃𝑛 ∈ ω
𝐴 ≈ 𝑛) |
40 | | ralnex 3167 |
. . 3
⊢
(∀𝑛 ∈
ω ¬ 𝐴 ≈
𝑛 ↔ ¬ ∃𝑛 ∈ ω 𝐴 ≈ 𝑛) |
41 | 39, 40 | bitr4i 277 |
. 2
⊢ (¬
𝐴 ∈ Fin ↔
∀𝑛 ∈ ω
¬ 𝐴 ≈ 𝑛) |
42 | 37, 41 | sylibr 233 |
1
⊢
(∀𝑛 ∈
ω 𝑛 ≼ 𝐴 → ¬ 𝐴 ∈ Fin) |