| Step | Hyp | Ref
| Expression |
| 1 | | nfra1 3284 |
. . . 4
⊢
Ⅎ𝑛∀𝑛 ∈ ω 𝑛 ≼ 𝐴 |
| 2 | | breq1 5146 |
. . . . . . 7
⊢ (𝑦 = 𝑛 → (𝑦 ≺ 𝐴 ↔ 𝑛 ≺ 𝐴)) |
| 3 | 2 | imbi2d 340 |
. . . . . 6
⊢ (𝑦 = 𝑛 → ((∀𝑛 ∈ ω 𝑛 ≼ 𝐴 → 𝑦 ≺ 𝐴) ↔ (∀𝑛 ∈ ω 𝑛 ≼ 𝐴 → 𝑛 ≺ 𝐴))) |
| 4 | | breq1 5146 |
. . . . . . 7
⊢ (𝑦 = ∅ → (𝑦 ≺ 𝐴 ↔ ∅ ≺ 𝐴)) |
| 5 | | breq1 5146 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → (𝑦 ≺ 𝐴 ↔ 𝑧 ≺ 𝐴)) |
| 6 | | breq1 5146 |
. . . . . . 7
⊢ (𝑦 = suc 𝑧 → (𝑦 ≺ 𝐴 ↔ suc 𝑧 ≺ 𝐴)) |
| 7 | | 1n0 8526 |
. . . . . . . . 9
⊢
1o ≠ ∅ |
| 8 | | 1onn 8678 |
. . . . . . . . . 10
⊢
1o ∈ ω |
| 9 | | 0sdomg 9144 |
. . . . . . . . . 10
⊢
(1o ∈ ω → (∅ ≺ 1o
↔ 1o ≠ ∅)) |
| 10 | 8, 9 | ax-mp 5 |
. . . . . . . . 9
⊢ (∅
≺ 1o ↔ 1o ≠ ∅) |
| 11 | 7, 10 | mpbir 231 |
. . . . . . . 8
⊢ ∅
≺ 1o |
| 12 | | breq1 5146 |
. . . . . . . . . 10
⊢ (𝑛 = 1o → (𝑛 ≼ 𝐴 ↔ 1o ≼ 𝐴)) |
| 13 | 12 | rspccv 3619 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
ω 𝑛 ≼ 𝐴 → (1o ∈
ω → 1o ≼ 𝐴)) |
| 14 | 8, 13 | mpi 20 |
. . . . . . . 8
⊢
(∀𝑛 ∈
ω 𝑛 ≼ 𝐴 → 1o ≼
𝐴) |
| 15 | | sdomdomtr 9150 |
. . . . . . . 8
⊢ ((∅
≺ 1o ∧ 1o ≼ 𝐴) → ∅ ≺ 𝐴) |
| 16 | 11, 14, 15 | sylancr 587 |
. . . . . . 7
⊢
(∀𝑛 ∈
ω 𝑛 ≼ 𝐴 → ∅ ≺ 𝐴) |
| 17 | | peano2 7912 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ω → suc 𝑧 ∈
ω) |
| 18 | | php4 9250 |
. . . . . . . . . . 11
⊢ (suc
𝑧 ∈ ω → suc
𝑧 ≺ suc suc 𝑧) |
| 19 | 17, 18 | syl 17 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ω → suc 𝑧 ≺ suc suc 𝑧) |
| 20 | | breq1 5146 |
. . . . . . . . . . . 12
⊢ (𝑛 = suc suc 𝑧 → (𝑛 ≼ 𝐴 ↔ suc suc 𝑧 ≼ 𝐴)) |
| 21 | 20 | rspccv 3619 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
ω 𝑛 ≼ 𝐴 → (suc suc 𝑧 ∈ ω → suc suc
𝑧 ≼ 𝐴)) |
| 22 | | peano2 7912 |
. . . . . . . . . . . 12
⊢ (suc
𝑧 ∈ ω → suc
suc 𝑧 ∈
ω) |
| 23 | 17, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ω → suc suc
𝑧 ∈
ω) |
| 24 | 21, 23 | impel 505 |
. . . . . . . . . 10
⊢
((∀𝑛 ∈
ω 𝑛 ≼ 𝐴 ∧ 𝑧 ∈ ω) → suc suc 𝑧 ≼ 𝐴) |
| 25 | | sdomdomtr 9150 |
. . . . . . . . . 10
⊢ ((suc
𝑧 ≺ suc suc 𝑧 ∧ suc suc 𝑧 ≼ 𝐴) → suc 𝑧 ≺ 𝐴) |
| 26 | 19, 24, 25 | syl2an2 686 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
ω 𝑛 ≼ 𝐴 ∧ 𝑧 ∈ ω) → suc 𝑧 ≺ 𝐴) |
| 27 | 26 | a1d 25 |
. . . . . . . 8
⊢
((∀𝑛 ∈
ω 𝑛 ≼ 𝐴 ∧ 𝑧 ∈ ω) → (𝑧 ≺ 𝐴 → suc 𝑧 ≺ 𝐴)) |
| 28 | 27 | expcom 413 |
. . . . . . 7
⊢ (𝑧 ∈ ω →
(∀𝑛 ∈ ω
𝑛 ≼ 𝐴 → (𝑧 ≺ 𝐴 → suc 𝑧 ≺ 𝐴))) |
| 29 | 4, 5, 6, 16, 28 | finds2 7920 |
. . . . . 6
⊢ (𝑦 ∈ ω →
(∀𝑛 ∈ ω
𝑛 ≼ 𝐴 → 𝑦 ≺ 𝐴)) |
| 30 | 3, 29 | vtoclga 3577 |
. . . . 5
⊢ (𝑛 ∈ ω →
(∀𝑛 ∈ ω
𝑛 ≼ 𝐴 → 𝑛 ≺ 𝐴)) |
| 31 | 30 | com12 32 |
. . . 4
⊢
(∀𝑛 ∈
ω 𝑛 ≼ 𝐴 → (𝑛 ∈ ω → 𝑛 ≺ 𝐴)) |
| 32 | 1, 31 | ralrimi 3257 |
. . 3
⊢
(∀𝑛 ∈
ω 𝑛 ≼ 𝐴 → ∀𝑛 ∈ ω 𝑛 ≺ 𝐴) |
| 33 | | sdomnen 9021 |
. . . . 5
⊢ (𝑛 ≺ 𝐴 → ¬ 𝑛 ≈ 𝐴) |
| 34 | | ensym 9043 |
. . . . 5
⊢ (𝐴 ≈ 𝑛 → 𝑛 ≈ 𝐴) |
| 35 | 33, 34 | nsyl 140 |
. . . 4
⊢ (𝑛 ≺ 𝐴 → ¬ 𝐴 ≈ 𝑛) |
| 36 | 35 | ralimi 3083 |
. . 3
⊢
(∀𝑛 ∈
ω 𝑛 ≺ 𝐴 → ∀𝑛 ∈ ω ¬ 𝐴 ≈ 𝑛) |
| 37 | 32, 36 | syl 17 |
. 2
⊢
(∀𝑛 ∈
ω 𝑛 ≼ 𝐴 → ∀𝑛 ∈ ω ¬ 𝐴 ≈ 𝑛) |
| 38 | | isfi 9016 |
. . . 4
⊢ (𝐴 ∈ Fin ↔ ∃𝑛 ∈ ω 𝐴 ≈ 𝑛) |
| 39 | 38 | notbii 320 |
. . 3
⊢ (¬
𝐴 ∈ Fin ↔ ¬
∃𝑛 ∈ ω
𝐴 ≈ 𝑛) |
| 40 | | ralnex 3072 |
. . 3
⊢
(∀𝑛 ∈
ω ¬ 𝐴 ≈
𝑛 ↔ ¬ ∃𝑛 ∈ ω 𝐴 ≈ 𝑛) |
| 41 | 39, 40 | bitr4i 278 |
. 2
⊢ (¬
𝐴 ∈ Fin ↔
∀𝑛 ∈ ω
¬ 𝐴 ≈ 𝑛) |
| 42 | 37, 41 | sylibr 234 |
1
⊢
(∀𝑛 ∈
ω 𝑛 ≼ 𝐴 → ¬ 𝐴 ∈ Fin) |