# Metamath Proof Explorer

## Theorem bnj1444

Description: Technical lemma for bnj60 . 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 bnj1444.1 ${⊢}{B}=\left\{{d}|\left({d}\subseteq {A}\wedge \forall {x}\in {d}\phantom{\rule{.4em}{0ex}}pred\left({x},{A},{R}\right)\subseteq {d}\right)\right\}$
bnj1444.2 ${⊢}{Y}=⟨{x},{{f}↾}_{pred\left({x},{A},{R}\right)}⟩$
bnj1444.3 ${⊢}{C}=\left\{{f}|\exists {d}\in {B}\phantom{\rule{.4em}{0ex}}\left({f}Fn{d}\wedge \forall {x}\in {d}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)={G}\left({Y}\right)\right)\right\}$
bnj1444.4 ${⊢}{\tau }↔\left({f}\in {C}\wedge \mathrm{dom}{f}=\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)\right)$
bnj1444.5 ${⊢}{D}=\left\{{x}\in {A}|¬\exists {f}\phantom{\rule{.4em}{0ex}}{\tau }\right\}$
bnj1444.6 ${⊢}{\psi }↔\left({R}FrSe{A}\wedge {D}\ne \varnothing \right)$
bnj1444.7 ${⊢}{\chi }↔\left({\psi }\wedge {x}\in {D}\wedge \forall {y}\in {D}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}\right)$
bnj1444.8 No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
bnj1444.9 No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
bnj1444.10 ${⊢}{P}=\bigcup {H}$
bnj1444.11 ${⊢}{Z}=⟨{x},{{P}↾}_{pred\left({x},{A},{R}\right)}⟩$
bnj1444.12 ${⊢}{Q}={P}\cup \left\{⟨{x},{G}\left({Z}\right)⟩\right\}$
bnj1444.13 ${⊢}{W}=⟨{z},{{Q}↾}_{pred\left({z},{A},{R}\right)}⟩$
bnj1444.14 ${⊢}{E}=\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)$
bnj1444.15 ${⊢}{\chi }\to {P}FntrCl\left({x},{A},{R}\right)$
bnj1444.16 ${⊢}{\chi }\to {Q}Fn\left(\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)\right)$
bnj1444.17 ${⊢}{\theta }↔\left({\chi }\wedge {z}\in {E}\right)$
bnj1444.18 ${⊢}{\eta }↔\left({\theta }\wedge {z}\in \left\{{x}\right\}\right)$
bnj1444.19 ${⊢}{\zeta }↔\left({\theta }\wedge {z}\in trCl\left({x},{A},{R}\right)\right)$
bnj1444.20 ${⊢}{\rho }↔\left({\zeta }\wedge {f}\in {H}\wedge {z}\in \mathrm{dom}{f}\right)$
Assertion bnj1444 ${⊢}{\rho }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\rho }$

### Proof

Step Hyp Ref Expression
1 bnj1444.1 ${⊢}{B}=\left\{{d}|\left({d}\subseteq {A}\wedge \forall {x}\in {d}\phantom{\rule{.4em}{0ex}}pred\left({x},{A},{R}\right)\subseteq {d}\right)\right\}$
2 bnj1444.2 ${⊢}{Y}=⟨{x},{{f}↾}_{pred\left({x},{A},{R}\right)}⟩$
3 bnj1444.3 ${⊢}{C}=\left\{{f}|\exists {d}\in {B}\phantom{\rule{.4em}{0ex}}\left({f}Fn{d}\wedge \forall {x}\in {d}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)={G}\left({Y}\right)\right)\right\}$
4 bnj1444.4 ${⊢}{\tau }↔\left({f}\in {C}\wedge \mathrm{dom}{f}=\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)\right)$
5 bnj1444.5 ${⊢}{D}=\left\{{x}\in {A}|¬\exists {f}\phantom{\rule{.4em}{0ex}}{\tau }\right\}$
6 bnj1444.6 ${⊢}{\psi }↔\left({R}FrSe{A}\wedge {D}\ne \varnothing \right)$
7 bnj1444.7 ${⊢}{\chi }↔\left({\psi }\wedge {x}\in {D}\wedge \forall {y}\in {D}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}\right)$
8 bnj1444.8 Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9 bnj1444.9 Could not format H = { f | E. y e. _pred ( x , A , R ) ta' } : No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
10 bnj1444.10 ${⊢}{P}=\bigcup {H}$
11 bnj1444.11 ${⊢}{Z}=⟨{x},{{P}↾}_{pred\left({x},{A},{R}\right)}⟩$
12 bnj1444.12 ${⊢}{Q}={P}\cup \left\{⟨{x},{G}\left({Z}\right)⟩\right\}$
13 bnj1444.13 ${⊢}{W}=⟨{z},{{Q}↾}_{pred\left({z},{A},{R}\right)}⟩$
14 bnj1444.14 ${⊢}{E}=\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)$
15 bnj1444.15 ${⊢}{\chi }\to {P}FntrCl\left({x},{A},{R}\right)$
16 bnj1444.16 ${⊢}{\chi }\to {Q}Fn\left(\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)\right)$
17 bnj1444.17 ${⊢}{\theta }↔\left({\chi }\wedge {z}\in {E}\right)$
18 bnj1444.18 ${⊢}{\eta }↔\left({\theta }\wedge {z}\in \left\{{x}\right\}\right)$
19 bnj1444.19 ${⊢}{\zeta }↔\left({\theta }\wedge {z}\in trCl\left({x},{A},{R}\right)\right)$
20 bnj1444.20 ${⊢}{\rho }↔\left({\zeta }\wedge {f}\in {H}\wedge {z}\in \mathrm{dom}{f}\right)$
21 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\psi }$
22 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{x}\in {D}$
23 nfra1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}$
24 21 22 23 nf3an ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {x}\in {D}\wedge \forall {y}\in {D}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}\right)$
25 7 24 nfxfr ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\chi }$
26 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{z}\in {E}$
27 25 26 nfan ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({\chi }\wedge {z}\in {E}\right)$
28 17 27 nfxfr ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\theta }$
29 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{z}\in trCl\left({x},{A},{R}\right)$
30 28 29 nfan ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({\theta }\wedge {z}\in trCl\left({x},{A},{R}\right)\right)$
31 19 30 nfxfr ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\zeta }$
32 nfre1 Could not format F/ y E. y e. _pred ( x , A , R ) ta' : No typesetting found for |- F/ y E. y e. _pred ( x , A , R ) ta' with typecode |-
33 32 nfab Could not format F/_ y { f | E. y e. _pred ( x , A , R ) ta' } : No typesetting found for |- F/_ y { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
34 9 33 nfcxfr ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{H}$
35 34 nfcri ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{f}\in {H}$
36 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{z}\in \mathrm{dom}{f}$
37 31 35 36 nf3an ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({\zeta }\wedge {f}\in {H}\wedge {z}\in \mathrm{dom}{f}\right)$
38 20 37 nfxfr ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\rho }$
39 38 nf5ri ${⊢}{\rho }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\rho }$