Proof of Theorem bnj168
Step | Hyp | Ref
| Expression |
1 | | bnj168.1 |
. . . . . . . . . 10
⊢ 𝐷 = (ω ∖
{∅}) |
2 | 1 | bnj158 32716 |
. . . . . . . . 9
⊢ (𝑛 ∈ 𝐷 → ∃𝑚 ∈ ω 𝑛 = suc 𝑚) |
3 | 2 | anim2i 617 |
. . . . . . . 8
⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷) → (𝑛 ≠ 1o ∧ ∃𝑚 ∈ ω 𝑛 = suc 𝑚)) |
4 | | r19.42v 3277 |
. . . . . . . 8
⊢
(∃𝑚 ∈
ω (𝑛 ≠
1o ∧ 𝑛 = suc
𝑚) ↔ (𝑛 ≠ 1o ∧
∃𝑚 ∈ ω
𝑛 = suc 𝑚)) |
5 | 3, 4 | sylibr 233 |
. . . . . . 7
⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷) → ∃𝑚 ∈ ω (𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚)) |
6 | | neeq1 3006 |
. . . . . . . . . . 11
⊢ (𝑛 = suc 𝑚 → (𝑛 ≠ 1o ↔ suc 𝑚 ≠
1o)) |
7 | 6 | biimpac 479 |
. . . . . . . . . 10
⊢ ((𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚) → suc 𝑚 ≠ 1o) |
8 | | df-1o 8284 |
. . . . . . . . . . . . 13
⊢
1o = suc ∅ |
9 | 8 | eqeq2i 2751 |
. . . . . . . . . . . 12
⊢ (suc
𝑚 = 1o ↔
suc 𝑚 = suc
∅) |
10 | | nnon 7708 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ω → 𝑚 ∈ On) |
11 | | 0elon 6312 |
. . . . . . . . . . . . 13
⊢ ∅
∈ On |
12 | | suc11 6362 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ On ∧ ∅ ∈
On) → (suc 𝑚 = suc
∅ ↔ 𝑚 =
∅)) |
13 | 10, 11, 12 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ω → (suc
𝑚 = suc ∅ ↔
𝑚 =
∅)) |
14 | 9, 13 | bitr2id 284 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ω → (𝑚 = ∅ ↔ suc 𝑚 =
1o)) |
15 | 14 | necon3bid 2988 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ω → (𝑚 ≠ ∅ ↔ suc 𝑚 ≠
1o)) |
16 | 7, 15 | syl5ibr 245 |
. . . . . . . . 9
⊢ (𝑚 ∈ ω → ((𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚) → 𝑚 ≠ ∅)) |
17 | 16 | ancld 551 |
. . . . . . . 8
⊢ (𝑚 ∈ ω → ((𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚) → ((𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚) ∧ 𝑚 ≠ ∅))) |
18 | 17 | reximia 3174 |
. . . . . . 7
⊢
(∃𝑚 ∈
ω (𝑛 ≠
1o ∧ 𝑛 = suc
𝑚) → ∃𝑚 ∈ ω ((𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚) ∧ 𝑚 ≠ ∅)) |
19 | 5, 18 | syl 17 |
. . . . . 6
⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷) → ∃𝑚 ∈ ω ((𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚) ∧ 𝑚 ≠ ∅)) |
20 | | anass 469 |
. . . . . . 7
⊢ (((𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚) ∧ 𝑚 ≠ ∅) ↔ (𝑛 ≠ 1o ∧ (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅))) |
21 | 20 | rexbii 3179 |
. . . . . 6
⊢
(∃𝑚 ∈
ω ((𝑛 ≠
1o ∧ 𝑛 = suc
𝑚) ∧ 𝑚 ≠ ∅) ↔ ∃𝑚 ∈ ω (𝑛 ≠ 1o ∧ (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅))) |
22 | 19, 21 | sylib 217 |
. . . . 5
⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷) → ∃𝑚 ∈ ω (𝑛 ≠ 1o ∧ (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅))) |
23 | | simpr 485 |
. . . . 5
⊢ ((𝑛 ≠ 1o ∧ (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅)) → (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅)) |
24 | 22, 23 | bnj31 32706 |
. . . 4
⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷) → ∃𝑚 ∈ ω (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅)) |
25 | | df-rex 3070 |
. . . 4
⊢
(∃𝑚 ∈
ω (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅) ↔ ∃𝑚(𝑚 ∈ ω ∧ (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅))) |
26 | 24, 25 | sylib 217 |
. . 3
⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷) → ∃𝑚(𝑚 ∈ ω ∧ (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅))) |
27 | | simpr 485 |
. . . . . . 7
⊢ ((𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅) → 𝑚 ≠ ∅) |
28 | 27 | anim2i 617 |
. . . . . 6
⊢ ((𝑚 ∈ ω ∧ (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅)) → (𝑚 ∈ ω ∧ 𝑚 ≠ ∅)) |
29 | 1 | eleq2i 2830 |
. . . . . . 7
⊢ (𝑚 ∈ 𝐷 ↔ 𝑚 ∈ (ω ∖
{∅})) |
30 | | eldifsn 4720 |
. . . . . . 7
⊢ (𝑚 ∈ (ω ∖
{∅}) ↔ (𝑚 ∈
ω ∧ 𝑚 ≠
∅)) |
31 | 29, 30 | bitr2i 275 |
. . . . . 6
⊢ ((𝑚 ∈ ω ∧ 𝑚 ≠ ∅) ↔ 𝑚 ∈ 𝐷) |
32 | 28, 31 | sylib 217 |
. . . . 5
⊢ ((𝑚 ∈ ω ∧ (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅)) → 𝑚 ∈ 𝐷) |
33 | | simprl 768 |
. . . . 5
⊢ ((𝑚 ∈ ω ∧ (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅)) → 𝑛 = suc 𝑚) |
34 | 32, 33 | jca 512 |
. . . 4
⊢ ((𝑚 ∈ ω ∧ (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅)) → (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚)) |
35 | 34 | eximi 1837 |
. . 3
⊢
(∃𝑚(𝑚 ∈ ω ∧ (𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅)) → ∃𝑚(𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚)) |
36 | 26, 35 | syl 17 |
. 2
⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷) → ∃𝑚(𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚)) |
37 | | df-rex 3070 |
. 2
⊢
(∃𝑚 ∈
𝐷 𝑛 = suc 𝑚 ↔ ∃𝑚(𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚)) |
38 | 36, 37 | sylibr 233 |
1
⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷) → ∃𝑚 ∈ 𝐷 𝑛 = suc 𝑚) |