# Metamath Proof Explorer

## Theorem bnj1520

Description: Technical lemma for bnj1500 . 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 bnj1520.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\}$
bnj1520.2 ${⊢}{Y}=⟨{x},{{f}↾}_{pred\left({x},{A},{R}\right)}⟩$
bnj1520.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\}$
bnj1520.4 ${⊢}{F}=\bigcup {C}$
Assertion bnj1520 ${⊢}{F}\left({x}\right)={G}\left(⟨{x},{{F}↾}_{pred\left({x},{A},{R}\right)}⟩\right)\to \forall {f}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={G}\left(⟨{x},{{F}↾}_{pred\left({x},{A},{R}\right)}⟩\right)$

### Proof

Step Hyp Ref Expression
1 bnj1520.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 bnj1520.2 ${⊢}{Y}=⟨{x},{{f}↾}_{pred\left({x},{A},{R}\right)}⟩$
3 bnj1520.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 bnj1520.4 ${⊢}{F}=\bigcup {C}$
5 3 bnj1317 ${⊢}{w}\in {C}\to \forall {f}\phantom{\rule{.4em}{0ex}}{w}\in {C}$
6 5 nfcii ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}{C}$
7 6 nfuni ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}\bigcup {C}$
8 4 7 nfcxfr ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}{F}$
9 nfcv ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}{x}$
10 8 9 nffv ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)$
11 nfcv ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}{G}$
12 nfcv ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}pred\left({x},{A},{R}\right)$
13 8 12 nfres ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{pred\left({x},{A},{R}\right)}\right)$
14 9 13 nfop ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}⟨{x},{{F}↾}_{pred\left({x},{A},{R}\right)}⟩$
15 11 14 nffv ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}{G}\left(⟨{x},{{F}↾}_{pred\left({x},{A},{R}\right)}⟩\right)$
16 10 15 nfeq ${⊢}Ⅎ{f}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={G}\left(⟨{x},{{F}↾}_{pred\left({x},{A},{R}\right)}⟩\right)$
17 16 nf5ri ${⊢}{F}\left({x}\right)={G}\left(⟨{x},{{F}↾}_{pred\left({x},{A},{R}\right)}⟩\right)\to \forall {f}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={G}\left(⟨{x},{{F}↾}_{pred\left({x},{A},{R}\right)}⟩\right)$