# Metamath Proof Explorer

## Theorem bnj1018

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). See bnj1018g for a less restrictive version requiring ax-13 . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1018.1 ${⊢}{\phi }↔{f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)$
bnj1018.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)$
bnj1018.3 ${⊢}{\chi }↔\left({n}\in {D}\wedge {f}Fn{n}\wedge {\phi }\wedge {\psi }\right)$
bnj1018.4 ${⊢}{\theta }↔\left({R}FrSe{A}\wedge {X}\in {A}\wedge {y}\in trCl\left({X},{A},{R}\right)\wedge {z}\in pred\left({y},{A},{R}\right)\right)$
bnj1018.5 ${⊢}{\tau }↔\left({m}\in \mathrm{\omega }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)$
bnj1018.7 No typesetting found for |- ( ph' <-> [. p / n ]. ph ) with typecode |-
bnj1018.8 No typesetting found for |- ( ps' <-> [. p / n ]. ps ) with typecode |-
bnj1018.9 No typesetting found for |- ( ch' <-> [. p / n ]. ch ) with typecode |-
bnj1018.10 No typesetting found for |- ( ph" <-> [. G / f ]. ph' ) with typecode |-
bnj1018.11 No typesetting found for |- ( ps" <-> [. G / f ]. ps' ) with typecode |-
bnj1018.12 No typesetting found for |- ( ch" <-> [. G / f ]. ch' ) with typecode |-
bnj1018.13 ${⊢}{D}=\mathrm{\omega }\setminus \left\{\varnothing \right\}$
bnj1018.14 ${⊢}{B}=\left\{{f}|\exists {n}\in {D}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {\phi }\wedge {\psi }\right)\right\}$
bnj1018.15 ${⊢}{C}=\bigcup _{{y}\in {f}\left({m}\right)}pred\left({y},{A},{R}\right)$
bnj1018.16 ${⊢}{G}={f}\cup \left\{⟨{n},{C}⟩\right\}$
bnj1018.26 No typesetting found for |- ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) with typecode |-
bnj1018.29 No typesetting found for |- ( ( th /\ ch /\ ta /\ et ) -> ch" ) with typecode |-
bnj1018.30 No typesetting found for |- ( ( th /\ ch /\ ta /\ et ) -> ( ch" /\ i e. _om /\ suc i e. p ) ) with typecode |-
Assertion bnj1018 ${⊢}\left({\theta }\wedge {\chi }\wedge {\eta }\wedge \exists {p}\phantom{\rule{.4em}{0ex}}{\tau }\right)\to {G}\left(\mathrm{suc}{i}\right)\subseteq trCl\left({X},{A},{R}\right)$

### Proof

Step Hyp Ref Expression
1 bnj1018.1 ${⊢}{\phi }↔{f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)$
2 bnj1018.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)$
3 bnj1018.3 ${⊢}{\chi }↔\left({n}\in {D}\wedge {f}Fn{n}\wedge {\phi }\wedge {\psi }\right)$
4 bnj1018.4 ${⊢}{\theta }↔\left({R}FrSe{A}\wedge {X}\in {A}\wedge {y}\in trCl\left({X},{A},{R}\right)\wedge {z}\in pred\left({y},{A},{R}\right)\right)$
5 bnj1018.5 ${⊢}{\tau }↔\left({m}\in \mathrm{\omega }\wedge {n}=\mathrm{suc}{m}\wedge {p}=\mathrm{suc}{n}\right)$
6 bnj1018.7 Could not format ( ph' <-> [. p / n ]. ph ) : No typesetting found for |- ( ph' <-> [. p / n ]. ph ) with typecode |-
7 bnj1018.8 Could not format ( ps' <-> [. p / n ]. ps ) : No typesetting found for |- ( ps' <-> [. p / n ]. ps ) with typecode |-
8 bnj1018.9 Could not format ( ch' <-> [. p / n ]. ch ) : No typesetting found for |- ( ch' <-> [. p / n ]. ch ) with typecode |-
9 bnj1018.10 Could not format ( ph" <-> [. G / f ]. ph' ) : No typesetting found for |- ( ph" <-> [. G / f ]. ph' ) with typecode |-
10 bnj1018.11 Could not format ( ps" <-> [. G / f ]. ps' ) : No typesetting found for |- ( ps" <-> [. G / f ]. ps' ) with typecode |-
11 bnj1018.12 Could not format ( ch" <-> [. G / f ]. ch' ) : No typesetting found for |- ( ch" <-> [. G / f ]. ch' ) with typecode |-
12 bnj1018.13 ${⊢}{D}=\mathrm{\omega }\setminus \left\{\varnothing \right\}$
13 bnj1018.14 ${⊢}{B}=\left\{{f}|\exists {n}\in {D}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {\phi }\wedge {\psi }\right)\right\}$
14 bnj1018.15 ${⊢}{C}=\bigcup _{{y}\in {f}\left({m}\right)}pred\left({y},{A},{R}\right)$
15 bnj1018.16 ${⊢}{G}={f}\cup \left\{⟨{n},{C}⟩\right\}$
16 bnj1018.26 Could not format ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) : No typesetting found for |- ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) with typecode |-
17 bnj1018.29 Could not format ( ( th /\ ch /\ ta /\ et ) -> ch" ) : No typesetting found for |- ( ( th /\ ch /\ ta /\ et ) -> ch" ) with typecode |-
18 bnj1018.30 Could not format ( ( th /\ ch /\ ta /\ et ) -> ( ch" /\ i e. _om /\ suc i e. p ) ) : No typesetting found for |- ( ( th /\ ch /\ ta /\ et ) -> ( ch" /\ i e. _om /\ suc i e. p ) ) with typecode |-
19 df-bnj17 ${⊢}\left({\theta }\wedge {\chi }\wedge {\eta }\wedge \exists {p}\phantom{\rule{.4em}{0ex}}{\tau }\right)↔\left(\left({\theta }\wedge {\chi }\wedge {\eta }\right)\wedge \exists {p}\phantom{\rule{.4em}{0ex}}{\tau }\right)$
20 bnj258 ${⊢}\left({\theta }\wedge {\chi }\wedge {\tau }\wedge {\eta }\right)↔\left(\left({\theta }\wedge {\chi }\wedge {\eta }\right)\wedge {\tau }\right)$
21 20 17 sylbir Could not format ( ( ( th /\ ch /\ et ) /\ ta ) -> ch" ) : No typesetting found for |- ( ( ( th /\ ch /\ et ) /\ ta ) -> ch" ) with typecode |-
22 21 ex Could not format ( ( th /\ ch /\ et ) -> ( ta -> ch" ) ) : No typesetting found for |- ( ( th /\ ch /\ et ) -> ( ta -> ch" ) ) with typecode |-
23 22 eximdv Could not format ( ( th /\ ch /\ et ) -> ( E. p ta -> E. p ch" ) ) : No typesetting found for |- ( ( th /\ ch /\ et ) -> ( E. p ta -> E. p ch" ) ) with typecode |-
24 3 8 11 13 15 bnj985v Could not format ( G e. B <-> E. p ch" ) : No typesetting found for |- ( G e. B <-> E. p ch" ) with typecode |-
25 23 24 syl6ibr ${⊢}\left({\theta }\wedge {\chi }\wedge {\eta }\right)\to \left(\exists {p}\phantom{\rule{.4em}{0ex}}{\tau }\to {G}\in {B}\right)$
26 25 imp ${⊢}\left(\left({\theta }\wedge {\chi }\wedge {\eta }\right)\wedge \exists {p}\phantom{\rule{.4em}{0ex}}{\tau }\right)\to {G}\in {B}$
27 19 26 sylbi ${⊢}\left({\theta }\wedge {\chi }\wedge {\eta }\wedge \exists {p}\phantom{\rule{.4em}{0ex}}{\tau }\right)\to {G}\in {B}$
28 bnj1019 ${⊢}\exists {p}\phantom{\rule{.4em}{0ex}}\left({\theta }\wedge {\chi }\wedge {\tau }\wedge {\eta }\right)↔\left({\theta }\wedge {\chi }\wedge {\eta }\wedge \exists {p}\phantom{\rule{.4em}{0ex}}{\tau }\right)$
29 18 simp3d ${⊢}\left({\theta }\wedge {\chi }\wedge {\tau }\wedge {\eta }\right)\to \mathrm{suc}{i}\in {p}$
30 16 bnj1235 Could not format ( ch" -> G Fn p ) : No typesetting found for |- ( ch" -> G Fn p ) with typecode |-
31 fndm ${⊢}{G}Fn{p}\to \mathrm{dom}{G}={p}$
32 17 30 31 3syl ${⊢}\left({\theta }\wedge {\chi }\wedge {\tau }\wedge {\eta }\right)\to \mathrm{dom}{G}={p}$
33 29 32 eleqtrrd ${⊢}\left({\theta }\wedge {\chi }\wedge {\tau }\wedge {\eta }\right)\to \mathrm{suc}{i}\in \mathrm{dom}{G}$
34 33 exlimiv ${⊢}\exists {p}\phantom{\rule{.4em}{0ex}}\left({\theta }\wedge {\chi }\wedge {\tau }\wedge {\eta }\right)\to \mathrm{suc}{i}\in \mathrm{dom}{G}$
35 28 34 sylbir ${⊢}\left({\theta }\wedge {\chi }\wedge {\eta }\wedge \exists {p}\phantom{\rule{.4em}{0ex}}{\tau }\right)\to \mathrm{suc}{i}\in \mathrm{dom}{G}$
36 15 bnj918 ${⊢}{G}\in \mathrm{V}$
37 vex ${⊢}{i}\in \mathrm{V}$
38 37 sucex ${⊢}\mathrm{suc}{i}\in \mathrm{V}$
39 1 2 12 13 36 38 bnj1015 ${⊢}\left({G}\in {B}\wedge \mathrm{suc}{i}\in \mathrm{dom}{G}\right)\to {G}\left(\mathrm{suc}{i}\right)\subseteq trCl\left({X},{A},{R}\right)$
40 27 35 39 syl2anc ${⊢}\left({\theta }\wedge {\chi }\wedge {\eta }\wedge \exists {p}\phantom{\rule{.4em}{0ex}}{\tau }\right)\to {G}\left(\mathrm{suc}{i}\right)\subseteq trCl\left({X},{A},{R}\right)$