# Metamath Proof Explorer

## Theorem bnj1466

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 bnj1466.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\}$
bnj1466.2 ${⊢}{Y}=⟨{x},{{f}↾}_{pred\left({x},{A},{R}\right)}⟩$
bnj1466.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\}$
bnj1466.4 ${⊢}{\tau }↔\left({f}\in {C}\wedge \mathrm{dom}{f}=\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)\right)$
bnj1466.5 ${⊢}{D}=\left\{{x}\in {A}|¬\exists {f}\phantom{\rule{.4em}{0ex}}{\tau }\right\}$
bnj1466.6 ${⊢}{\psi }↔\left({R}FrSe{A}\wedge {D}\ne \varnothing \right)$
bnj1466.7 ${⊢}{\chi }↔\left({\psi }\wedge {x}\in {D}\wedge \forall {y}\in {D}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}\right)$
bnj1466.8 No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
bnj1466.9 No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
bnj1466.10 ${⊢}{P}=\bigcup {H}$
bnj1466.11 ${⊢}{Z}=⟨{x},{{P}↾}_{pred\left({x},{A},{R}\right)}⟩$
bnj1466.12 ${⊢}{Q}={P}\cup \left\{⟨{x},{G}\left({Z}\right)⟩\right\}$
Assertion bnj1466 ${⊢}{w}\in {Q}\to \forall {f}\phantom{\rule{.4em}{0ex}}{w}\in {Q}$

### Proof

Step Hyp Ref Expression
1 bnj1466.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 bnj1466.2 ${⊢}{Y}=⟨{x},{{f}↾}_{pred\left({x},{A},{R}\right)}⟩$
3 bnj1466.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 bnj1466.4 ${⊢}{\tau }↔\left({f}\in {C}\wedge \mathrm{dom}{f}=\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)\right)$
5 bnj1466.5 ${⊢}{D}=\left\{{x}\in {A}|¬\exists {f}\phantom{\rule{.4em}{0ex}}{\tau }\right\}$
6 bnj1466.6 ${⊢}{\psi }↔\left({R}FrSe{A}\wedge {D}\ne \varnothing \right)$
7 bnj1466.7 ${⊢}{\chi }↔\left({\psi }\wedge {x}\in {D}\wedge \forall {y}\in {D}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}\right)$
8 bnj1466.8 Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9 bnj1466.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 bnj1466.10 ${⊢}{P}=\bigcup {H}$
11 bnj1466.11 ${⊢}{Z}=⟨{x},{{P}↾}_{pred\left({x},{A},{R}\right)}⟩$
12 bnj1466.12 ${⊢}{Q}={P}\cup \left\{⟨{x},{G}\left({Z}\right)⟩\right\}$
13 9 bnj1317 ${⊢}{w}\in {H}\to \forall {f}\phantom{\rule{.4em}{0ex}}{w}\in {H}$
14 13 nfcii ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}{H}$
15 14 nfuni ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}\bigcup {H}$
16 10 15 nfcxfr ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}{P}$
17 nfcv ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}{x}$
18 nfcv ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}{G}$
19 nfcv ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}pred\left({x},{A},{R}\right)$
20 16 19 nfres ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}\left({{P}↾}_{pred\left({x},{A},{R}\right)}\right)$
21 17 20 nfop ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}⟨{x},{{P}↾}_{pred\left({x},{A},{R}\right)}⟩$
22 11 21 nfcxfr ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}{Z}$
23 18 22 nffv ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}{G}\left({Z}\right)$
24 17 23 nfop ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}⟨{x},{G}\left({Z}\right)⟩$
25 24 nfsn ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}\left\{⟨{x},{G}\left({Z}\right)⟩\right\}$
26 16 25 nfun ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}\left({P}\cup \left\{⟨{x},{G}\left({Z}\right)⟩\right\}\right)$
27 12 26 nfcxfr ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}{Q}$
28 27 nfcrii ${⊢}{w}\in {Q}\to \forall {f}\phantom{\rule{.4em}{0ex}}{w}\in {Q}$