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