# Metamath Proof Explorer

## Theorem bnj558

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 bnj558.3 ${⊢}{D}=\mathrm{\omega }\setminus \left\{\varnothing \right\}$
bnj558.16 ${⊢}{G}={f}\cup \left\{⟨{m},\bigcup _{{y}\in {f}\left({p}\right)}pred\left({y},{A},{R}\right)⟩\right\}$
bnj558.17 No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
bnj558.18 ${⊢}{\sigma }↔\left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\wedge {p}\in {m}\right)$
bnj558.19 ${⊢}{\eta }↔\left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\wedge {p}\in \mathrm{\omega }\wedge {m}=\mathrm{suc}{p}\right)$
bnj558.20 ${⊢}{\zeta }↔\left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {n}\wedge {m}=\mathrm{suc}{i}\right)$
bnj558.21 ${⊢}{B}=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)$
bnj558.22 ${⊢}{C}=\bigcup _{{y}\in {f}\left({p}\right)}pred\left({y},{A},{R}\right)$
bnj558.23 ${⊢}{K}=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)$
bnj558.24 ${⊢}{L}=\bigcup _{{y}\in {G}\left({p}\right)}pred\left({y},{A},{R}\right)$
bnj558.25 ${⊢}{G}={f}\cup \left\{⟨{m},{C}⟩\right\}$
bnj558.28 No typesetting found for |- ( ph' <-> ( f  (/) ) = _pred ( x , A , R ) ) with typecode |-
bnj558.29 No typesetting found for |- ( ps' <-> A. i e. _om ( suc i e. m -> ( f  suc i ) = U_ y e. ( f  i ) _pred ( y , A , R ) ) ) with typecode |-
bnj558.36 ${⊢}\left({R}FrSe{A}\wedge {\tau }\wedge {\sigma }\right)\to {G}Fn{n}$
Assertion bnj558 ${⊢}\left({R}FrSe{A}\wedge {\tau }\wedge {\eta }\wedge {\zeta }\right)\to {G}\left(\mathrm{suc}{i}\right)={K}$

### Proof

Step Hyp Ref Expression
1 bnj558.3 ${⊢}{D}=\mathrm{\omega }\setminus \left\{\varnothing \right\}$
2 bnj558.16 ${⊢}{G}={f}\cup \left\{⟨{m},\bigcup _{{y}\in {f}\left({p}\right)}pred\left({y},{A},{R}\right)⟩\right\}$
3 bnj558.17 Could not format ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
4 bnj558.18 ${⊢}{\sigma }↔\left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\wedge {p}\in {m}\right)$
5 bnj558.19 ${⊢}{\eta }↔\left({m}\in {D}\wedge {n}=\mathrm{suc}{m}\wedge {p}\in \mathrm{\omega }\wedge {m}=\mathrm{suc}{p}\right)$
6 bnj558.20 ${⊢}{\zeta }↔\left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {n}\wedge {m}=\mathrm{suc}{i}\right)$
7 bnj558.21 ${⊢}{B}=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)$
8 bnj558.22 ${⊢}{C}=\bigcup _{{y}\in {f}\left({p}\right)}pred\left({y},{A},{R}\right)$
9 bnj558.23 ${⊢}{K}=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)$
10 bnj558.24 ${⊢}{L}=\bigcup _{{y}\in {G}\left({p}\right)}pred\left({y},{A},{R}\right)$
11 bnj558.25 ${⊢}{G}={f}\cup \left\{⟨{m},{C}⟩\right\}$
12 bnj558.28 Could not format ( ph' <-> ( f  (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph' <-> ( f  (/) ) = _pred ( x , A , R ) ) with typecode |-
13 bnj558.29 Could not format ( ps' <-> A. i e. _om ( suc i e. m -> ( f  suc i ) = U_ y e. ( f  i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps' <-> A. i e. _om ( suc i e. m -> ( f  suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode |-
14 bnj558.36 ${⊢}\left({R}FrSe{A}\wedge {\tau }\wedge {\sigma }\right)\to {G}Fn{n}$
15 1 2 3 4 5 6 7 8 9 10 11 12 13 14 bnj557 ${⊢}\left({R}FrSe{A}\wedge {\tau }\wedge {\eta }\wedge {\zeta }\right)\to {G}\left({m}\right)={L}$
16 bnj422 ${⊢}\left({R}FrSe{A}\wedge {\tau }\wedge {\eta }\wedge {\zeta }\right)↔\left({\eta }\wedge {\zeta }\wedge {R}FrSe{A}\wedge {\tau }\right)$
17 bnj253 ${⊢}\left({\eta }\wedge {\zeta }\wedge {R}FrSe{A}\wedge {\tau }\right)↔\left(\left({\eta }\wedge {\zeta }\right)\wedge {R}FrSe{A}\wedge {\tau }\right)$
18 16 17 bitri ${⊢}\left({R}FrSe{A}\wedge {\tau }\wedge {\eta }\wedge {\zeta }\right)↔\left(\left({\eta }\wedge {\zeta }\right)\wedge {R}FrSe{A}\wedge {\tau }\right)$
19 18 simp1bi ${⊢}\left({R}FrSe{A}\wedge {\tau }\wedge {\eta }\wedge {\zeta }\right)\to \left({\eta }\wedge {\zeta }\right)$
20 5 6 9 10 9 10 bnj554 ${⊢}\left({\eta }\wedge {\zeta }\right)\to \left({G}\left({m}\right)={L}↔{G}\left(\mathrm{suc}{i}\right)={K}\right)$
21 19 20 syl ${⊢}\left({R}FrSe{A}\wedge {\tau }\wedge {\eta }\wedge {\zeta }\right)\to \left({G}\left({m}\right)={L}↔{G}\left(\mathrm{suc}{i}\right)={K}\right)$
22 15 21 mpbid ${⊢}\left({R}FrSe{A}\wedge {\tau }\wedge {\eta }\wedge {\zeta }\right)\to {G}\left(\mathrm{suc}{i}\right)={K}$