Step |
Hyp |
Ref |
Expression |
1 |
|
bnj168.1 |
⊢ 𝐷 = ( ω ∖ { ∅ } ) |
2 |
1
|
bnj158 |
⊢ ( 𝑛 ∈ 𝐷 → ∃ 𝑚 ∈ ω 𝑛 = suc 𝑚 ) |
3 |
2
|
anim2i |
⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ( 𝑛 ≠ 1o ∧ ∃ 𝑚 ∈ ω 𝑛 = suc 𝑚 ) ) |
4 |
|
r19.42v |
⊢ ( ∃ 𝑚 ∈ ω ( 𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚 ) ↔ ( 𝑛 ≠ 1o ∧ ∃ 𝑚 ∈ ω 𝑛 = suc 𝑚 ) ) |
5 |
3 4
|
sylibr |
⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑚 ∈ ω ( 𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚 ) ) |
6 |
|
neeq1 |
⊢ ( 𝑛 = suc 𝑚 → ( 𝑛 ≠ 1o ↔ suc 𝑚 ≠ 1o ) ) |
7 |
6
|
biimpac |
⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚 ) → suc 𝑚 ≠ 1o ) |
8 |
|
df-1o |
⊢ 1o = suc ∅ |
9 |
8
|
eqeq2i |
⊢ ( suc 𝑚 = 1o ↔ suc 𝑚 = suc ∅ ) |
10 |
|
nnon |
⊢ ( 𝑚 ∈ ω → 𝑚 ∈ On ) |
11 |
|
0elon |
⊢ ∅ ∈ On |
12 |
|
suc11 |
⊢ ( ( 𝑚 ∈ On ∧ ∅ ∈ On ) → ( suc 𝑚 = suc ∅ ↔ 𝑚 = ∅ ) ) |
13 |
10 11 12
|
sylancl |
⊢ ( 𝑚 ∈ ω → ( suc 𝑚 = suc ∅ ↔ 𝑚 = ∅ ) ) |
14 |
9 13
|
syl5rbb |
⊢ ( 𝑚 ∈ ω → ( 𝑚 = ∅ ↔ suc 𝑚 = 1o ) ) |
15 |
14
|
necon3bid |
⊢ ( 𝑚 ∈ ω → ( 𝑚 ≠ ∅ ↔ suc 𝑚 ≠ 1o ) ) |
16 |
7 15
|
syl5ibr |
⊢ ( 𝑚 ∈ ω → ( ( 𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚 ) → 𝑚 ≠ ∅ ) ) |
17 |
16
|
ancld |
⊢ ( 𝑚 ∈ ω → ( ( 𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚 ) → ( ( 𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚 ) ∧ 𝑚 ≠ ∅ ) ) ) |
18 |
17
|
reximia |
⊢ ( ∃ 𝑚 ∈ ω ( 𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚 ) → ∃ 𝑚 ∈ ω ( ( 𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚 ) ∧ 𝑚 ≠ ∅ ) ) |
19 |
5 18
|
syl |
⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑚 ∈ ω ( ( 𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚 ) ∧ 𝑚 ≠ ∅ ) ) |
20 |
|
anass |
⊢ ( ( ( 𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚 ) ∧ 𝑚 ≠ ∅ ) ↔ ( 𝑛 ≠ 1o ∧ ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) ) |
21 |
20
|
rexbii |
⊢ ( ∃ 𝑚 ∈ ω ( ( 𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚 ) ∧ 𝑚 ≠ ∅ ) ↔ ∃ 𝑚 ∈ ω ( 𝑛 ≠ 1o ∧ ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) ) |
22 |
19 21
|
sylib |
⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑚 ∈ ω ( 𝑛 ≠ 1o ∧ ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) ) |
23 |
|
simpr |
⊢ ( ( 𝑛 ≠ 1o ∧ ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) → ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) |
24 |
22 23
|
bnj31 |
⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑚 ∈ ω ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) |
25 |
|
df-rex |
⊢ ( ∃ 𝑚 ∈ ω ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ↔ ∃ 𝑚 ( 𝑚 ∈ ω ∧ ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) ) |
26 |
24 25
|
sylib |
⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑚 ( 𝑚 ∈ ω ∧ ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) ) |
27 |
|
simpr |
⊢ ( ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) → 𝑚 ≠ ∅ ) |
28 |
27
|
anim2i |
⊢ ( ( 𝑚 ∈ ω ∧ ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) → ( 𝑚 ∈ ω ∧ 𝑚 ≠ ∅ ) ) |
29 |
1
|
eleq2i |
⊢ ( 𝑚 ∈ 𝐷 ↔ 𝑚 ∈ ( ω ∖ { ∅ } ) ) |
30 |
|
eldifsn |
⊢ ( 𝑚 ∈ ( ω ∖ { ∅ } ) ↔ ( 𝑚 ∈ ω ∧ 𝑚 ≠ ∅ ) ) |
31 |
29 30
|
bitr2i |
⊢ ( ( 𝑚 ∈ ω ∧ 𝑚 ≠ ∅ ) ↔ 𝑚 ∈ 𝐷 ) |
32 |
28 31
|
sylib |
⊢ ( ( 𝑚 ∈ ω ∧ ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) → 𝑚 ∈ 𝐷 ) |
33 |
|
simprl |
⊢ ( ( 𝑚 ∈ ω ∧ ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) → 𝑛 = suc 𝑚 ) |
34 |
32 33
|
jca |
⊢ ( ( 𝑚 ∈ ω ∧ ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) → ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ) ) |
35 |
34
|
eximi |
⊢ ( ∃ 𝑚 ( 𝑚 ∈ ω ∧ ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) → ∃ 𝑚 ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ) ) |
36 |
26 35
|
syl |
⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑚 ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ) ) |
37 |
|
df-rex |
⊢ ( ∃ 𝑚 ∈ 𝐷 𝑛 = suc 𝑚 ↔ ∃ 𝑚 ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ) ) |
38 |
36 37
|
sylibr |
⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑚 ∈ 𝐷 𝑛 = suc 𝑚 ) |