Proof of Theorem bnj168
Step | Hyp | Ref
| Expression |
1 | | bnj168.1 |
. . . . . . . . . 10
⊢ 𝐷 = (ω ∖
{∅}) |
2 | 1 | bnj158 30051 |
. . . . . . . . 9
⊢ (𝑛 ∈ 𝐷 → ∃𝑚 ∈ ω 𝑛 = suc 𝑚) |
3 | 2 | anim2i 591 |
. . . . . . . 8
⊢ ((𝑛 ≠ 1𝑜
∧ 𝑛 ∈ 𝐷) → (𝑛 ≠ 1𝑜 ∧
∃𝑚 ∈ ω
𝑛 = suc 𝑚)) |
4 | | r19.42v 3073 |
. . . . . . . 8
⊢
(∃𝑚 ∈
ω (𝑛 ≠
1𝑜 ∧ 𝑛 = suc 𝑚) ↔ (𝑛 ≠ 1𝑜 ∧
∃𝑚 ∈ ω
𝑛 = suc 𝑚)) |
5 | 3, 4 | sylibr 223 |
. . . . . . 7
⊢ ((𝑛 ≠ 1𝑜
∧ 𝑛 ∈ 𝐷) → ∃𝑚 ∈ ω (𝑛 ≠ 1𝑜
∧ 𝑛 = suc 𝑚)) |
6 | | neeq1 2844 |
. . . . . . . . . . 11
⊢ (𝑛 = suc 𝑚 → (𝑛 ≠ 1𝑜 ↔ suc 𝑚 ≠
1𝑜)) |
7 | 6 | biimpac 502 |
. . . . . . . . . 10
⊢ ((𝑛 ≠ 1𝑜
∧ 𝑛 = suc 𝑚) → suc 𝑚 ≠ 1𝑜) |
8 | | df-1o 7447 |
. . . . . . . . . . . . 13
⊢
1𝑜 = suc ∅ |
9 | 8 | eqeq2i 2622 |
. . . . . . . . . . . 12
⊢ (suc
𝑚 = 1𝑜
↔ suc 𝑚 = suc
∅) |
10 | | nnon 6963 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ω → 𝑚 ∈ On) |
11 | | 0elon 5695 |
. . . . . . . . . . . . 13
⊢ ∅
∈ On |
12 | | suc11 5748 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ On ∧ ∅ ∈
On) → (suc 𝑚 = suc
∅ ↔ 𝑚 =
∅)) |
13 | 10, 11, 12 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ω → (suc
𝑚 = suc ∅ ↔
𝑚 =
∅)) |
14 | 9, 13 | syl5rbb 272 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ω → (𝑚 = ∅ ↔ suc 𝑚 =
1𝑜)) |
15 | 14 | necon3bid 2826 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ω → (𝑚 ≠ ∅ ↔ suc 𝑚 ≠
1𝑜)) |
16 | 7, 15 | syl5ibr 235 |
. . . . . . . . 9
⊢ (𝑚 ∈ ω → ((𝑛 ≠ 1𝑜
∧ 𝑛 = suc 𝑚) → 𝑚 ≠ ∅)) |
17 | 16 | ancld 574 |
. . . . . . . 8
⊢ (𝑚 ∈ ω → ((𝑛 ≠ 1𝑜
∧ 𝑛 = suc 𝑚) → ((𝑛 ≠ 1𝑜 ∧ 𝑛 = suc 𝑚) ∧ 𝑚 ≠ ∅))) |
18 | 17 | reximia 2992 |
. . . . . . 7
⊢
(∃𝑚 ∈
ω (𝑛 ≠
1𝑜 ∧ 𝑛 = suc 𝑚) → ∃𝑚 ∈ ω ((𝑛 ≠ 1𝑜 ∧ 𝑛 = suc 𝑚) ∧ 𝑚 ≠ ∅)) |
19 | 5, 18 | syl 17 |
. . . . . 6
⊢ ((𝑛 ≠ 1𝑜
∧ 𝑛 ∈ 𝐷) → ∃𝑚 ∈ ω ((𝑛 ≠ 1𝑜
∧ 𝑛 = suc 𝑚) ∧ 𝑚 ≠ ∅)) |
20 | | anass 679 |
. . . . . . 7
⊢ (((𝑛 ≠ 1𝑜
∧ 𝑛 = suc 𝑚) ∧ 𝑚 ≠ ∅) ↔ (𝑛 ≠ 1𝑜 ∧ (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅))) |
21 | 20 | rexbii 3023 |
. . . . . 6
⊢
(∃𝑚 ∈
ω ((𝑛 ≠
1𝑜 ∧ 𝑛 = suc 𝑚) ∧ 𝑚 ≠ ∅) ↔ ∃𝑚 ∈ ω (𝑛 ≠ 1𝑜
∧ (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅))) |
22 | 19, 21 | sylib 207 |
. . . . 5
⊢ ((𝑛 ≠ 1𝑜
∧ 𝑛 ∈ 𝐷) → ∃𝑚 ∈ ω (𝑛 ≠ 1𝑜
∧ (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅))) |
23 | | simpr 476 |
. . . . 5
⊢ ((𝑛 ≠ 1𝑜
∧ (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅)) → (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅)) |
24 | 22, 23 | bnj31 30039 |
. . . 4
⊢ ((𝑛 ≠ 1𝑜
∧ 𝑛 ∈ 𝐷) → ∃𝑚 ∈ ω (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅)) |
25 | | df-rex 2902 |
. . . 4
⊢
(∃𝑚 ∈
ω (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅) ↔ ∃𝑚(𝑚 ∈ ω ∧ (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅))) |
26 | 24, 25 | sylib 207 |
. . 3
⊢ ((𝑛 ≠ 1𝑜
∧ 𝑛 ∈ 𝐷) → ∃𝑚(𝑚 ∈ ω ∧ (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅))) |
27 | | simpr 476 |
. . . . . . 7
⊢ ((𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅) → 𝑚 ≠ ∅) |
28 | 27 | anim2i 591 |
. . . . . 6
⊢ ((𝑚 ∈ ω ∧ (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅)) → (𝑚 ∈ ω ∧ 𝑚 ≠ ∅)) |
29 | 1 | eleq2i 2680 |
. . . . . . 7
⊢ (𝑚 ∈ 𝐷 ↔ 𝑚 ∈ (ω ∖
{∅})) |
30 | | eldifsn 4260 |
. . . . . . 7
⊢ (𝑚 ∈ (ω ∖
{∅}) ↔ (𝑚 ∈
ω ∧ 𝑚 ≠
∅)) |
31 | 29, 30 | bitr2i 264 |
. . . . . 6
⊢ ((𝑚 ∈ ω ∧ 𝑚 ≠ ∅) ↔ 𝑚 ∈ 𝐷) |
32 | 28, 31 | sylib 207 |
. . . . 5
⊢ ((𝑚 ∈ ω ∧ (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅)) → 𝑚 ∈ 𝐷) |
33 | | simprl 790 |
. . . . 5
⊢ ((𝑚 ∈ ω ∧ (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅)) → 𝑛 = suc 𝑚) |
34 | 32, 33 | jca 553 |
. . . 4
⊢ ((𝑚 ∈ ω ∧ (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅)) → (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚)) |
35 | 34 | eximi 1752 |
. . 3
⊢
(∃𝑚(𝑚 ∈ ω ∧ (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅)) → ∃𝑚(𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚)) |
36 | 26, 35 | syl 17 |
. 2
⊢ ((𝑛 ≠ 1𝑜
∧ 𝑛 ∈ 𝐷) → ∃𝑚(𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚)) |
37 | | df-rex 2902 |
. 2
⊢
(∃𝑚 ∈
𝐷 𝑛 = suc 𝑚 ↔ ∃𝑚(𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚)) |
38 | 36, 37 | sylibr 223 |
1
⊢ ((𝑛 ≠ 1𝑜
∧ 𝑛 ∈ 𝐷) → ∃𝑚 ∈ 𝐷 𝑛 = suc 𝑚) |