# Metamath Proof Explorer

## Theorem bnj964

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 bnj964.2 ${⊢}{\psi }↔\forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)$
bnj964.3 ${⊢}{\chi }↔\left({n}\in {D}\wedge {f}Fn{n}\wedge {\phi }\wedge {\psi }\right)$
bnj964.5 No typesetting found for |- ( ps' <-> [. p / n ]. ps ) with typecode |-
bnj964.8 No typesetting found for |- ( ps" <-> [. G / f ]. ps' ) with typecode |-
bnj964.12 ${⊢}{C}=\bigcup _{{y}\in {f}\left({m}\right)}pred\left({y},{A},{R}\right)$
bnj964.13 ${⊢}{G}={f}\cup \left\{⟨{n},{C}⟩\right\}$
bnj964.96 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge \mathrm{suc}{i}\in {n}\right)\right)\to {G}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)$
bnj964.165 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\right)\to {G}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)$
Assertion bnj964 Could not format assertion : No typesetting found for |- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ps" ) with typecode |-

### Proof

Step Hyp Ref Expression
1 bnj964.2 ${⊢}{\psi }↔\forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)$
2 bnj964.3 ${⊢}{\chi }↔\left({n}\in {D}\wedge {f}Fn{n}\wedge {\phi }\wedge {\psi }\right)$
3 bnj964.5 Could not format ( ps' <-> [. p / n ]. ps ) : No typesetting found for |- ( ps' <-> [. p / n ]. ps ) with typecode |-
4 bnj964.8 Could not format ( ps" <-> [. G / f ]. ps' ) : No typesetting found for |- ( ps" <-> [. G / f ]. ps' ) with typecode |-
5 bnj964.12 ${⊢}{C}=\bigcup _{{y}\in {f}\left({m}\right)}pred\left({y},{A},{R}\right)$
6 bnj964.13 ${⊢}{G}={f}\cup \left\{⟨{n},{C}⟩\right\}$
7 bnj964.96 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge \mathrm{suc}{i}\in {n}\right)\right)\to {G}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)$
8 bnj964.165 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\right)\to {G}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)$
9 nfv ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}\left({R}FrSe{A}\wedge {X}\in {A}\right)$
10 1 bnj1095 ${⊢}{\psi }\to \forall {i}\phantom{\rule{.4em}{0ex}}{\psi }$
11 10 2 bnj1096 ${⊢}{\chi }\to \forall {i}\phantom{\rule{.4em}{0ex}}{\chi }$
12 11 nf5i ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{\chi }$
13 nfv ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{n}=\mathrm{suc}{m}$
14 nfv ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{p}=\mathrm{suc}{n}$
15 12 13 14 nf3an ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}\left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)$
16 9 15 nfan ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\right)$
17 bnj255 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge {i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)↔\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\right)$
18 bnj645 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge {i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\to \mathrm{suc}{i}\in {p}$
19 simp3 ${⊢}\left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\to {p}=\mathrm{suc}{n}$
20 19 bnj706 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge {i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\to {p}=\mathrm{suc}{n}$
21 eleq2 ${⊢}{p}=\mathrm{suc}{n}\to \left(\mathrm{suc}{i}\in {p}↔\mathrm{suc}{i}\in \mathrm{suc}{n}\right)$
22 21 biimpac ${⊢}\left(\mathrm{suc}{i}\in {p}\wedge {p}=\mathrm{suc}{n}\right)\to \mathrm{suc}{i}\in \mathrm{suc}{n}$
23 elsuci ${⊢}\mathrm{suc}{i}\in \mathrm{suc}{n}\to \left(\mathrm{suc}{i}\in {n}\vee \mathrm{suc}{i}={n}\right)$
24 eqcom ${⊢}\mathrm{suc}{i}={n}↔{n}=\mathrm{suc}{i}$
25 24 orbi2i ${⊢}\left(\mathrm{suc}{i}\in {n}\vee \mathrm{suc}{i}={n}\right)↔\left(\mathrm{suc}{i}\in {n}\vee {n}=\mathrm{suc}{i}\right)$
26 23 25 sylib ${⊢}\mathrm{suc}{i}\in \mathrm{suc}{n}\to \left(\mathrm{suc}{i}\in {n}\vee {n}=\mathrm{suc}{i}\right)$
27 22 26 syl ${⊢}\left(\mathrm{suc}{i}\in {p}\wedge {p}=\mathrm{suc}{n}\right)\to \left(\mathrm{suc}{i}\in {n}\vee {n}=\mathrm{suc}{i}\right)$
28 18 20 27 syl2anc ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge {i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\to \left(\mathrm{suc}{i}\in {n}\vee {n}=\mathrm{suc}{i}\right)$
29 df-3an ${⊢}\left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge \mathrm{suc}{i}\in {n}\right)↔\left(\left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\wedge \mathrm{suc}{i}\in {n}\right)$
30 29 3anbi3i ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge \mathrm{suc}{i}\in {n}\right)\right)↔\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left(\left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\wedge \mathrm{suc}{i}\in {n}\right)\right)$
31 bnj255 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\wedge \mathrm{suc}{i}\in {n}\right)↔\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left(\left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\wedge \mathrm{suc}{i}\in {n}\right)\right)$
32 30 31 bitr4i ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge \mathrm{suc}{i}\in {n}\right)\right)↔\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\wedge \mathrm{suc}{i}\in {n}\right)$
33 bnj345 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\wedge \mathrm{suc}{i}\in {n}\right)↔\left(\mathrm{suc}{i}\in {n}\wedge \left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\right)$
34 bnj252 ${⊢}\left(\mathrm{suc}{i}\in {n}\wedge \left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\right)↔\left(\mathrm{suc}{i}\in {n}\wedge \left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\right)\right)$
35 32 33 34 3bitri ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge \mathrm{suc}{i}\in {n}\right)\right)↔\left(\mathrm{suc}{i}\in {n}\wedge \left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\right)\right)$
36 17 anbi2i ${⊢}\left(\mathrm{suc}{i}\in {n}\wedge \left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge {i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\right)↔\left(\mathrm{suc}{i}\in {n}\wedge \left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\right)\right)$
37 35 36 bitr4i ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge \mathrm{suc}{i}\in {n}\right)\right)↔\left(\mathrm{suc}{i}\in {n}\wedge \left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge {i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\right)$
38 37 7 sylbir ${⊢}\left(\mathrm{suc}{i}\in {n}\wedge \left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge {i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\right)\to {G}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)$
39 38 ex ${⊢}\mathrm{suc}{i}\in {n}\to \left(\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge {i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\to {G}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)\right)$
40 df-3an ${⊢}\left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)↔\left(\left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\wedge {n}=\mathrm{suc}{i}\right)$
41 40 3anbi3i ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\right)↔\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left(\left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\wedge {n}=\mathrm{suc}{i}\right)\right)$
42 bnj255 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\wedge {n}=\mathrm{suc}{i}\right)↔\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left(\left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\wedge {n}=\mathrm{suc}{i}\right)\right)$
43 41 42 bitr4i ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\right)↔\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\wedge {n}=\mathrm{suc}{i}\right)$
44 bnj345 ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\wedge {n}=\mathrm{suc}{i}\right)↔\left({n}=\mathrm{suc}{i}\wedge \left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\right)$
45 bnj252 ${⊢}\left({n}=\mathrm{suc}{i}\wedge \left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\right)↔\left({n}=\mathrm{suc}{i}\wedge \left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\right)\right)$
46 43 44 45 3bitri ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\right)↔\left({n}=\mathrm{suc}{i}\wedge \left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\right)\right)$
47 17 anbi2i ${⊢}\left({n}=\mathrm{suc}{i}\wedge \left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge {i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\right)↔\left({n}=\mathrm{suc}{i}\wedge \left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\right)\right)$
48 46 47 bitr4i ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\wedge {n}=\mathrm{suc}{i}\right)\right)↔\left({n}=\mathrm{suc}{i}\wedge \left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge {i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\right)$
49 48 8 sylbir ${⊢}\left({n}=\mathrm{suc}{i}\wedge \left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge {i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\right)\to {G}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)$
50 49 ex ${⊢}{n}=\mathrm{suc}{i}\to \left(\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge {i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\to {G}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)\right)$
51 39 50 jaoi ${⊢}\left(\mathrm{suc}{i}\in {n}\vee {n}=\mathrm{suc}{i}\right)\to \left(\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge {i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\to {G}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)\right)$
52 28 51 mpcom ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge {i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\to {G}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)$
53 17 52 sylbir ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\wedge \left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\right)\to {G}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)$
54 53 3expia ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\right)\to \left(\left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\to {G}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)\right)$
55 16 54 alrimi ${⊢}\left(\left({R}FrSe{A}\wedge {X}\in {A}\right)\wedge \left({\chi }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)\right)\to \forall {i}\phantom{\rule{.4em}{0ex}}\left(\left({i}\in \mathrm{\omega }\wedge \mathrm{suc}{i}\in {p}\right)\to {G}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {G}\left({i}\right)}pred\left({y},{A},{R}\right)\right)$
56 vex ${⊢}{p}\in \mathrm{V}$
57 1 3 56 bnj539 Could not format ( ps' <-> A. i e. _om ( suc i e. p -> ( f  suc i ) = U_ y e. ( f  i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps' <-> A. i e. _om ( suc i e. p -> ( f  suc i ) = U_ y e. ( f  i ) _pred ( y , A , R ) ) ) with typecode |-
58 57 4 5 6 bnj965 Could not format ( ps" <-> A. i e. _om ( suc i e. p -> ( G  suc i ) = U_ y e. ( G  i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps" <-> A. i e. _om ( suc i e. p -> ( G  suc i ) = U_ y e. ( G  i ) _pred ( y , A , R ) ) ) with typecode |-
59 58 bnj115 Could not format ( ps" <-> A. i ( ( i e. _om /\ suc i e. p ) -> ( G  suc i ) = U_ y e. ( G  i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps" <-> A. i ( ( i e. _om /\ suc i e. p ) -> ( G  suc i ) = U_ y e. ( G  i ) _pred ( y , A , R ) ) ) with typecode |-
60 55 59 sylibr Could not format ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ps" ) : No typesetting found for |- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ps" ) with typecode |-