# Metamath Proof Explorer

## Theorem bnj1501

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 bnj1501.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\}$
bnj1501.2 ${⊢}{Y}=⟨{x},{{f}↾}_{pred\left({x},{A},{R}\right)}⟩$
bnj1501.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\}$
bnj1501.4 ${⊢}{F}=\bigcup {C}$
bnj1501.5 ${⊢}{\phi }↔\left({R}FrSe{A}\wedge {x}\in {A}\right)$
bnj1501.6 ${⊢}{\psi }↔\left({\phi }\wedge {f}\in {C}\wedge {x}\in \mathrm{dom}{f}\right)$
bnj1501.7 ${⊢}{\chi }↔\left({\psi }\wedge {d}\in {B}\wedge \mathrm{dom}{f}={d}\right)$
Assertion bnj1501 ${⊢}{R}FrSe{A}\to \forall {x}\in {A}\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 bnj1501.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 bnj1501.2 ${⊢}{Y}=⟨{x},{{f}↾}_{pred\left({x},{A},{R}\right)}⟩$
3 bnj1501.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 bnj1501.4 ${⊢}{F}=\bigcup {C}$
5 bnj1501.5 ${⊢}{\phi }↔\left({R}FrSe{A}\wedge {x}\in {A}\right)$
6 bnj1501.6 ${⊢}{\psi }↔\left({\phi }\wedge {f}\in {C}\wedge {x}\in \mathrm{dom}{f}\right)$
7 bnj1501.7 ${⊢}{\chi }↔\left({\psi }\wedge {d}\in {B}\wedge \mathrm{dom}{f}={d}\right)$
8 5 simprbi ${⊢}{\phi }\to {x}\in {A}$
9 1 2 3 4 bnj60 ${⊢}{R}FrSe{A}\to {F}Fn{A}$
10 fndm ${⊢}{F}Fn{A}\to \mathrm{dom}{F}={A}$
11 9 10 syl ${⊢}{R}FrSe{A}\to \mathrm{dom}{F}={A}$
12 5 11 bnj832 ${⊢}{\phi }\to \mathrm{dom}{F}={A}$
13 8 12 eleqtrrd ${⊢}{\phi }\to {x}\in \mathrm{dom}{F}$
14 4 dmeqi ${⊢}\mathrm{dom}{F}=\mathrm{dom}\bigcup {C}$
15 3 bnj1317 ${⊢}{w}\in {C}\to \forall {f}\phantom{\rule{.4em}{0ex}}{w}\in {C}$
16 15 bnj1400 ${⊢}\mathrm{dom}\bigcup {C}=\bigcup _{{f}\in {C}}\mathrm{dom}{f}$
17 14 16 eqtri ${⊢}\mathrm{dom}{F}=\bigcup _{{f}\in {C}}\mathrm{dom}{f}$
18 13 17 eleqtrdi ${⊢}{\phi }\to {x}\in \bigcup _{{f}\in {C}}\mathrm{dom}{f}$
19 18 bnj1405 ${⊢}{\phi }\to \exists {f}\in {C}\phantom{\rule{.4em}{0ex}}{x}\in \mathrm{dom}{f}$
20 19 6 bnj1209 ${⊢}{\phi }\to \exists {f}\phantom{\rule{.4em}{0ex}}{\psi }$
21 3 bnj1436 ${⊢}{f}\in {C}\to \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)$
22 21 bnj1299 ${⊢}{f}\in {C}\to \exists {d}\in {B}\phantom{\rule{.4em}{0ex}}{f}Fn{d}$
23 fndm ${⊢}{f}Fn{d}\to \mathrm{dom}{f}={d}$
24 22 23 bnj31 ${⊢}{f}\in {C}\to \exists {d}\in {B}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{f}={d}$
25 6 24 bnj836 ${⊢}{\psi }\to \exists {d}\in {B}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{f}={d}$
26 1 2 3 4 5 6 bnj1518 ${⊢}{\psi }\to \forall {d}\phantom{\rule{.4em}{0ex}}{\psi }$
27 25 7 26 bnj1521 ${⊢}{\psi }\to \exists {d}\phantom{\rule{.4em}{0ex}}{\chi }$
28 9 bnj930 ${⊢}{R}FrSe{A}\to \mathrm{Fun}{F}$
29 5 28 bnj832 ${⊢}{\phi }\to \mathrm{Fun}{F}$
30 6 29 bnj835 ${⊢}{\psi }\to \mathrm{Fun}{F}$
31 elssuni ${⊢}{f}\in {C}\to {f}\subseteq \bigcup {C}$
32 31 4 sseqtrrdi ${⊢}{f}\in {C}\to {f}\subseteq {F}$
33 6 32 bnj836 ${⊢}{\psi }\to {f}\subseteq {F}$
34 6 simp3bi ${⊢}{\psi }\to {x}\in \mathrm{dom}{f}$
35 30 33 34 bnj1502 ${⊢}{\psi }\to {F}\left({x}\right)={f}\left({x}\right)$
36 1 2 3 bnj1514 ${⊢}{f}\in {C}\to \forall {x}\in \mathrm{dom}{f}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)={G}\left({Y}\right)$
37 6 36 bnj836 ${⊢}{\psi }\to \forall {x}\in \mathrm{dom}{f}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)={G}\left({Y}\right)$
38 37 34 bnj1294 ${⊢}{\psi }\to {f}\left({x}\right)={G}\left({Y}\right)$
39 35 38 eqtrd ${⊢}{\psi }\to {F}\left({x}\right)={G}\left({Y}\right)$
40 7 39 bnj835 ${⊢}{\chi }\to {F}\left({x}\right)={G}\left({Y}\right)$
41 7 30 bnj835 ${⊢}{\chi }\to \mathrm{Fun}{F}$
42 7 33 bnj835 ${⊢}{\chi }\to {f}\subseteq {F}$
43 1 bnj1517 ${⊢}{d}\in {B}\to \forall {x}\in {d}\phantom{\rule{.4em}{0ex}}pred\left({x},{A},{R}\right)\subseteq {d}$
44 7 43 bnj836 ${⊢}{\chi }\to \forall {x}\in {d}\phantom{\rule{.4em}{0ex}}pred\left({x},{A},{R}\right)\subseteq {d}$
45 7 34 bnj835 ${⊢}{\chi }\to {x}\in \mathrm{dom}{f}$
46 7 simp3bi ${⊢}{\chi }\to \mathrm{dom}{f}={d}$
47 45 46 eleqtrd ${⊢}{\chi }\to {x}\in {d}$
48 44 47 bnj1294 ${⊢}{\chi }\to pred\left({x},{A},{R}\right)\subseteq {d}$
49 48 46 sseqtrrd ${⊢}{\chi }\to pred\left({x},{A},{R}\right)\subseteq \mathrm{dom}{f}$
50 41 42 49 bnj1503 ${⊢}{\chi }\to {{F}↾}_{pred\left({x},{A},{R}\right)}={{f}↾}_{pred\left({x},{A},{R}\right)}$
51 50 opeq2d ${⊢}{\chi }\to ⟨{x},{{F}↾}_{pred\left({x},{A},{R}\right)}⟩=⟨{x},{{f}↾}_{pred\left({x},{A},{R}\right)}⟩$
52 51 2 syl6eqr ${⊢}{\chi }\to ⟨{x},{{F}↾}_{pred\left({x},{A},{R}\right)}⟩={Y}$
53 52 fveq2d ${⊢}{\chi }\to {G}\left(⟨{x},{{F}↾}_{pred\left({x},{A},{R}\right)}⟩\right)={G}\left({Y}\right)$
54 40 53 eqtr4d ${⊢}{\chi }\to {F}\left({x}\right)={G}\left(⟨{x},{{F}↾}_{pred\left({x},{A},{R}\right)}⟩\right)$
55 27 54 bnj593 ${⊢}{\psi }\to \exists {d}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={G}\left(⟨{x},{{F}↾}_{pred\left({x},{A},{R}\right)}⟩\right)$
56 1 2 3 4 bnj1519 ${⊢}{F}\left({x}\right)={G}\left(⟨{x},{{F}↾}_{pred\left({x},{A},{R}\right)}⟩\right)\to \forall {d}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={G}\left(⟨{x},{{F}↾}_{pred\left({x},{A},{R}\right)}⟩\right)$
57 55 56 bnj1397 ${⊢}{\psi }\to {F}\left({x}\right)={G}\left(⟨{x},{{F}↾}_{pred\left({x},{A},{R}\right)}⟩\right)$
58 20 57 bnj593 ${⊢}{\phi }\to \exists {f}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={G}\left(⟨{x},{{F}↾}_{pred\left({x},{A},{R}\right)}⟩\right)$
59 1 2 3 4 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)$
60 58 59 bnj1397 ${⊢}{\phi }\to {F}\left({x}\right)={G}\left(⟨{x},{{F}↾}_{pred\left({x},{A},{R}\right)}⟩\right)$
61 5 60 bnj1459 ${⊢}{R}FrSe{A}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={G}\left(⟨{x},{{F}↾}_{pred\left({x},{A},{R}\right)}⟩\right)$