# Metamath Proof Explorer

## Theorem bnj986

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj986.3 ${⊢}{\chi }↔\left({n}\in {D}\wedge {f}Fn{n}\wedge {\phi }\wedge {\psi }\right)$
bnj986.10 ${⊢}{D}=\mathrm{\omega }\setminus \left\{\varnothing \right\}$
bnj986.15 ${⊢}{\tau }↔\left({m}\in \mathrm{\omega }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)$
Assertion bnj986 ${⊢}{\chi }\to \exists {m}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{\tau }$

### Proof

Step Hyp Ref Expression
1 bnj986.3 ${⊢}{\chi }↔\left({n}\in {D}\wedge {f}Fn{n}\wedge {\phi }\wedge {\psi }\right)$
2 bnj986.10 ${⊢}{D}=\mathrm{\omega }\setminus \left\{\varnothing \right\}$
3 bnj986.15 ${⊢}{\tau }↔\left({m}\in \mathrm{\omega }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)$
4 2 bnj158 ${⊢}{n}\in {D}\to \exists {m}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{n}=\mathrm{suc}{m}$
5 1 4 bnj769 ${⊢}{\chi }\to \exists {m}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{n}=\mathrm{suc}{m}$
6 5 bnj1196 ${⊢}{\chi }\to \exists {m}\phantom{\rule{.4em}{0ex}}\left({m}\in \mathrm{\omega }\wedge {n}=\mathrm{suc}{m}\right)$
7 vex ${⊢}{n}\in \mathrm{V}$
8 7 sucex ${⊢}\mathrm{suc}{n}\in \mathrm{V}$
9 8 isseti ${⊢}\exists {p}\phantom{\rule{.4em}{0ex}}{p}=\mathrm{suc}{n}$
10 6 9 jctir ${⊢}{\chi }\to \left(\exists {m}\phantom{\rule{.4em}{0ex}}\left({m}\in \mathrm{\omega }\wedge {n}=\mathrm{suc}{m}\right)\wedge \exists {p}\phantom{\rule{.4em}{0ex}}{p}=\mathrm{suc}{n}\right)$
11 exdistr ${⊢}\exists {m}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}\left(\left({m}\in \mathrm{\omega }\wedge {n}=\mathrm{suc}{m}\right)\wedge {p}=\mathrm{suc}{n}\right)↔\exists {m}\phantom{\rule{.4em}{0ex}}\left(\left({m}\in \mathrm{\omega }\wedge {n}=\mathrm{suc}{m}\right)\wedge \exists {p}\phantom{\rule{.4em}{0ex}}{p}=\mathrm{suc}{n}\right)$
12 19.41v ${⊢}\exists {m}\phantom{\rule{.4em}{0ex}}\left(\left({m}\in \mathrm{\omega }\wedge {n}=\mathrm{suc}{m}\right)\wedge \exists {p}\phantom{\rule{.4em}{0ex}}{p}=\mathrm{suc}{n}\right)↔\left(\exists {m}\phantom{\rule{.4em}{0ex}}\left({m}\in \mathrm{\omega }\wedge {n}=\mathrm{suc}{m}\right)\wedge \exists {p}\phantom{\rule{.4em}{0ex}}{p}=\mathrm{suc}{n}\right)$
13 11 12 bitr2i ${⊢}\left(\exists {m}\phantom{\rule{.4em}{0ex}}\left({m}\in \mathrm{\omega }\wedge {n}=\mathrm{suc}{m}\right)\wedge \exists {p}\phantom{\rule{.4em}{0ex}}{p}=\mathrm{suc}{n}\right)↔\exists {m}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}\left(\left({m}\in \mathrm{\omega }\wedge {n}=\mathrm{suc}{m}\right)\wedge {p}=\mathrm{suc}{n}\right)$
14 10 13 sylib ${⊢}{\chi }\to \exists {m}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}\left(\left({m}\in \mathrm{\omega }\wedge {n}=\mathrm{suc}{m}\right)\wedge {p}=\mathrm{suc}{n}\right)$
15 df-3an ${⊢}\left({m}\in \mathrm{\omega }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)↔\left(\left({m}\in \mathrm{\omega }\wedge {n}=\mathrm{suc}{m}\right)\wedge {p}=\mathrm{suc}{n}\right)$
16 3 15 bitri ${⊢}{\tau }↔\left(\left({m}\in \mathrm{\omega }\wedge {n}=\mathrm{suc}{m}\right)\wedge {p}=\mathrm{suc}{n}\right)$
17 16 2exbii ${⊢}\exists {m}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{\tau }↔\exists {m}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}\left(\left({m}\in \mathrm{\omega }\wedge {n}=\mathrm{suc}{m}\right)\wedge {p}=\mathrm{suc}{n}\right)$
18 14 17 sylibr ${⊢}{\chi }\to \exists {m}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{\tau }$