# Metamath Proof Explorer

## Theorem bnj554

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 bnj554.19 ${⊢}{\eta }↔\left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\wedge {p}\in \mathrm{\omega }\wedge {m}=\mathrm{suc}{p}\right)$
bnj554.20 ${⊢}{\zeta }↔\left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {n}\wedge {m}=\mathrm{suc}{i}\right)$
bnj554.21 ${⊢}{K}=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)$
bnj554.22 ${⊢}{L}=\bigcup _{{y}\in {G}\left({p}\right)}pred\left({y},{A},{R}\right)$
bnj554.23 ${⊢}{K}=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)$
bnj554.24 ${⊢}{L}=\bigcup _{{y}\in {G}\left({p}\right)}pred\left({y},{A},{R}\right)$
Assertion bnj554 ${⊢}\left({\eta }\wedge {\zeta }\right)\to \left({G}\left({m}\right)={L}↔{G}\left(\mathrm{suc}{i}\right)={K}\right)$

### Proof

Step Hyp Ref Expression
1 bnj554.19 ${⊢}{\eta }↔\left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\wedge {p}\in \mathrm{\omega }\wedge {m}=\mathrm{suc}{p}\right)$
2 bnj554.20 ${⊢}{\zeta }↔\left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {n}\wedge {m}=\mathrm{suc}{i}\right)$
3 bnj554.21 ${⊢}{K}=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)$
4 bnj554.22 ${⊢}{L}=\bigcup _{{y}\in {G}\left({p}\right)}pred\left({y},{A},{R}\right)$
5 bnj554.23 ${⊢}{K}=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)$
6 bnj554.24 ${⊢}{L}=\bigcup _{{y}\in {G}\left({p}\right)}pred\left({y},{A},{R}\right)$
7 1 bnj1254 ${⊢}{\eta }\to {m}=\mathrm{suc}{p}$
8 2 simp3bi ${⊢}{\zeta }\to {m}=\mathrm{suc}{i}$
9 simpr ${⊢}\left({m}=\mathrm{suc}{p}\wedge {m}=\mathrm{suc}{i}\right)\to {m}=\mathrm{suc}{i}$
10 bnj551 ${⊢}\left({m}=\mathrm{suc}{p}\wedge {m}=\mathrm{suc}{i}\right)\to {p}={i}$
11 fveq2 ${⊢}{m}=\mathrm{suc}{i}\to {G}\left({m}\right)={G}\left(\mathrm{suc}{i}\right)$
12 fveq2 ${⊢}{p}={i}\to {G}\left({p}\right)={G}\left({i}\right)$
13 iuneq1 ${⊢}{G}\left({p}\right)={G}\left({i}\right)\to \bigcup _{{y}\in {G}\left({p}\right)}pred\left({y},{A},{R}\right)=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)$
14 13 6 5 3eqtr4g ${⊢}{G}\left({p}\right)={G}\left({i}\right)\to {L}={K}$
15 12 14 syl ${⊢}{p}={i}\to {L}={K}$
16 11 15 eqeqan12d ${⊢}\left({m}=\mathrm{suc}{i}\wedge {p}={i}\right)\to \left({G}\left({m}\right)={L}↔{G}\left(\mathrm{suc}{i}\right)={K}\right)$
17 9 10 16 syl2anc ${⊢}\left({m}=\mathrm{suc}{p}\wedge {m}=\mathrm{suc}{i}\right)\to \left({G}\left({m}\right)={L}↔{G}\left(\mathrm{suc}{i}\right)={K}\right)$
18 7 8 17 syl2an ${⊢}\left({\eta }\wedge {\zeta }\right)\to \left({G}\left({m}\right)={L}↔{G}\left(\mathrm{suc}{i}\right)={K}\right)$