# Metamath Proof Explorer

## Theorem bnj168

Description: First-order logic and set theory. Revised to remove dependence on ax-reg . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Revised by NM, 21-Dec-2016) (New usage is discouraged.)

Ref Expression
Hypothesis bnj168.1 ${⊢}{D}=\mathrm{\omega }\setminus \left\{\varnothing \right\}$
Assertion bnj168 ${⊢}\left({n}\ne {1}_{𝑜}\wedge {n}\in {D}\right)\to \exists {m}\in {D}\phantom{\rule{.4em}{0ex}}{n}=\mathrm{suc}{m}$

### Proof

Step Hyp Ref Expression
1 bnj168.1 ${⊢}{D}=\mathrm{\omega }\setminus \left\{\varnothing \right\}$
2 1 bnj158 ${⊢}{n}\in {D}\to \exists {m}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{n}=\mathrm{suc}{m}$
3 2 anim2i ${⊢}\left({n}\ne {1}_{𝑜}\wedge {n}\in {D}\right)\to \left({n}\ne {1}_{𝑜}\wedge \exists {m}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{n}=\mathrm{suc}{m}\right)$
4 r19.42v ${⊢}\exists {m}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({n}\ne {1}_{𝑜}\wedge {n}=\mathrm{suc}{m}\right)↔\left({n}\ne {1}_{𝑜}\wedge \exists {m}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{n}=\mathrm{suc}{m}\right)$
5 3 4 sylibr ${⊢}\left({n}\ne {1}_{𝑜}\wedge {n}\in {D}\right)\to \exists {m}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({n}\ne {1}_{𝑜}\wedge {n}=\mathrm{suc}{m}\right)$
6 neeq1 ${⊢}{n}=\mathrm{suc}{m}\to \left({n}\ne {1}_{𝑜}↔\mathrm{suc}{m}\ne {1}_{𝑜}\right)$
7 6 biimpac ${⊢}\left({n}\ne {1}_{𝑜}\wedge {n}=\mathrm{suc}{m}\right)\to \mathrm{suc}{m}\ne {1}_{𝑜}$
8 df-1o ${⊢}{1}_{𝑜}=\mathrm{suc}\varnothing$
9 8 eqeq2i ${⊢}\mathrm{suc}{m}={1}_{𝑜}↔\mathrm{suc}{m}=\mathrm{suc}\varnothing$
10 nnon ${⊢}{m}\in \mathrm{\omega }\to {m}\in \mathrm{On}$
11 0elon ${⊢}\varnothing \in \mathrm{On}$
12 suc11 ${⊢}\left({m}\in \mathrm{On}\wedge \varnothing \in \mathrm{On}\right)\to \left(\mathrm{suc}{m}=\mathrm{suc}\varnothing ↔{m}=\varnothing \right)$
13 10 11 12 sylancl ${⊢}{m}\in \mathrm{\omega }\to \left(\mathrm{suc}{m}=\mathrm{suc}\varnothing ↔{m}=\varnothing \right)$
14 9 13 syl5rbb ${⊢}{m}\in \mathrm{\omega }\to \left({m}=\varnothing ↔\mathrm{suc}{m}={1}_{𝑜}\right)$
15 14 necon3bid ${⊢}{m}\in \mathrm{\omega }\to \left({m}\ne \varnothing ↔\mathrm{suc}{m}\ne {1}_{𝑜}\right)$
16 7 15 syl5ibr ${⊢}{m}\in \mathrm{\omega }\to \left(\left({n}\ne {1}_{𝑜}\wedge {n}=\mathrm{suc}{m}\right)\to {m}\ne \varnothing \right)$
17 16 ancld ${⊢}{m}\in \mathrm{\omega }\to \left(\left({n}\ne {1}_{𝑜}\wedge {n}=\mathrm{suc}{m}\right)\to \left(\left({n}\ne {1}_{𝑜}\wedge {n}=\mathrm{suc}{m}\right)\wedge {m}\ne \varnothing \right)\right)$
18 17 reximia ${⊢}\exists {m}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({n}\ne {1}_{𝑜}\wedge {n}=\mathrm{suc}{m}\right)\to \exists {m}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\left({n}\ne {1}_{𝑜}\wedge {n}=\mathrm{suc}{m}\right)\wedge {m}\ne \varnothing \right)$
19 5 18 syl ${⊢}\left({n}\ne {1}_{𝑜}\wedge {n}\in {D}\right)\to \exists {m}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\left({n}\ne {1}_{𝑜}\wedge {n}=\mathrm{suc}{m}\right)\wedge {m}\ne \varnothing \right)$
20 anass ${⊢}\left(\left({n}\ne {1}_{𝑜}\wedge {n}=\mathrm{suc}{m}\right)\wedge {m}\ne \varnothing \right)↔\left({n}\ne {1}_{𝑜}\wedge \left({n}=\mathrm{suc}{m}\wedge {m}\ne \varnothing \right)\right)$
21 20 rexbii ${⊢}\exists {m}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\left({n}\ne {1}_{𝑜}\wedge {n}=\mathrm{suc}{m}\right)\wedge {m}\ne \varnothing \right)↔\exists {m}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({n}\ne {1}_{𝑜}\wedge \left({n}=\mathrm{suc}{m}\wedge {m}\ne \varnothing \right)\right)$
22 19 21 sylib ${⊢}\left({n}\ne {1}_{𝑜}\wedge {n}\in {D}\right)\to \exists {m}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({n}\ne {1}_{𝑜}\wedge \left({n}=\mathrm{suc}{m}\wedge {m}\ne \varnothing \right)\right)$
23 simpr ${⊢}\left({n}\ne {1}_{𝑜}\wedge \left({n}=\mathrm{suc}{m}\wedge {m}\ne \varnothing \right)\right)\to \left({n}=\mathrm{suc}{m}\wedge {m}\ne \varnothing \right)$
24 22 23 bnj31 ${⊢}\left({n}\ne {1}_{𝑜}\wedge {n}\in {D}\right)\to \exists {m}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({n}=\mathrm{suc}{m}\wedge {m}\ne \varnothing \right)$
25 df-rex ${⊢}\exists {m}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({n}=\mathrm{suc}{m}\wedge {m}\ne \varnothing \right)↔\exists {m}\phantom{\rule{.4em}{0ex}}\left({m}\in \mathrm{\omega }\wedge \left({n}=\mathrm{suc}{m}\wedge {m}\ne \varnothing \right)\right)$
26 24 25 sylib ${⊢}\left({n}\ne {1}_{𝑜}\wedge {n}\in {D}\right)\to \exists {m}\phantom{\rule{.4em}{0ex}}\left({m}\in \mathrm{\omega }\wedge \left({n}=\mathrm{suc}{m}\wedge {m}\ne \varnothing \right)\right)$
27 simpr ${⊢}\left({n}=\mathrm{suc}{m}\wedge {m}\ne \varnothing \right)\to {m}\ne \varnothing$
28 27 anim2i ${⊢}\left({m}\in \mathrm{\omega }\wedge \left({n}=\mathrm{suc}{m}\wedge {m}\ne \varnothing \right)\right)\to \left({m}\in \mathrm{\omega }\wedge {m}\ne \varnothing \right)$
29 1 eleq2i ${⊢}{m}\in {D}↔{m}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)$
30 eldifsn ${⊢}{m}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)↔\left({m}\in \mathrm{\omega }\wedge {m}\ne \varnothing \right)$
31 29 30 bitr2i ${⊢}\left({m}\in \mathrm{\omega }\wedge {m}\ne \varnothing \right)↔{m}\in {D}$
32 28 31 sylib ${⊢}\left({m}\in \mathrm{\omega }\wedge \left({n}=\mathrm{suc}{m}\wedge {m}\ne \varnothing \right)\right)\to {m}\in {D}$
33 simprl ${⊢}\left({m}\in \mathrm{\omega }\wedge \left({n}=\mathrm{suc}{m}\wedge {m}\ne \varnothing \right)\right)\to {n}=\mathrm{suc}{m}$
34 32 33 jca ${⊢}\left({m}\in \mathrm{\omega }\wedge \left({n}=\mathrm{suc}{m}\wedge {m}\ne \varnothing \right)\right)\to \left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\right)$
35 34 eximi ${⊢}\exists {m}\phantom{\rule{.4em}{0ex}}\left({m}\in \mathrm{\omega }\wedge \left({n}=\mathrm{suc}{m}\wedge {m}\ne \varnothing \right)\right)\to \exists {m}\phantom{\rule{.4em}{0ex}}\left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\right)$
36 26 35 syl ${⊢}\left({n}\ne {1}_{𝑜}\wedge {n}\in {D}\right)\to \exists {m}\phantom{\rule{.4em}{0ex}}\left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\right)$
37 df-rex ${⊢}\exists {m}\in {D}\phantom{\rule{.4em}{0ex}}{n}=\mathrm{suc}{m}↔\exists {m}\phantom{\rule{.4em}{0ex}}\left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\right)$
38 36 37 sylibr ${⊢}\left({n}\ne {1}_{𝑜}\wedge {n}\in {D}\right)\to \exists {m}\in {D}\phantom{\rule{.4em}{0ex}}{n}=\mathrm{suc}{m}$