Metamath Proof Explorer

Theorem bnj556

Description: Technical lemma for bnj852 . 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 bnj556.18 ${⊢}{\sigma }↔\left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\wedge {p}\in {m}\right)$
bnj556.19 ${⊢}{\eta }↔\left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\wedge {p}\in \mathrm{\omega }\wedge {m}=\mathrm{suc}{p}\right)$
Assertion bnj556 ${⊢}{\eta }\to {\sigma }$

Proof

Step Hyp Ref Expression
1 bnj556.18 ${⊢}{\sigma }↔\left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\wedge {p}\in {m}\right)$
2 bnj556.19 ${⊢}{\eta }↔\left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\wedge {p}\in \mathrm{\omega }\wedge {m}=\mathrm{suc}{p}\right)$
3 vex ${⊢}{p}\in \mathrm{V}$
4 3 bnj216 ${⊢}{m}=\mathrm{suc}{p}\to {p}\in {m}$
5 4 3anim3i ${⊢}\left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\wedge {m}=\mathrm{suc}{p}\right)\to \left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\wedge {p}\in {m}\right)$
6 5 adantr ${⊢}\left(\left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\wedge {m}=\mathrm{suc}{p}\right)\wedge {p}\in \mathrm{\omega }\right)\to \left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\wedge {p}\in {m}\right)$
7 bnj258 ${⊢}\left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\wedge {p}\in \mathrm{\omega }\wedge {m}=\mathrm{suc}{p}\right)↔\left(\left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\wedge {m}=\mathrm{suc}{p}\right)\wedge {p}\in \mathrm{\omega }\right)$
8 2 7 bitri ${⊢}{\eta }↔\left(\left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\wedge {m}=\mathrm{suc}{p}\right)\wedge {p}\in \mathrm{\omega }\right)$
9 6 8 1 3imtr4i ${⊢}{\eta }\to {\sigma }$