Theorem bnj1312

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	bnj1312.1	$$⊢B=\left\{d|\left(d\subseteq A\wedge \forall x\in dpred\left(x,A,R\right)\subseteq d\right)\right\}$$
	bnj1312.2	$$⊢Y=⟨x,{f\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
	bnj1312.3	$$⊢C=\left\{f|\exists d\in B\left(fFnd\wedge \forall x\in df\left(x\right)=G\left(Y\right)\right)\right\}$$
	bnj1312.4	$$⊢\tau \leftrightarrow \left(f\in C\wedge \mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
	bnj1312.5	$$⊢D=\left\{x\in A|\neg \exists f\tau \right\}$$
	bnj1312.6	$$⊢\psi \leftrightarrow \left(RFrSeA\wedge D\ne \varnothing \right)$$
	bnj1312.7	$$⊢\chi \leftrightarrow \left(\psi \wedge x\in D\wedge \forall y\in D\neg yRx\right)$$
	bnj1312.8	No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
	bnj1312.9	No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
	bnj1312.10	$$⊢P=\bigcup H$$
	bnj1312.11	$$⊢Z=⟨x,{P\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
	bnj1312.12	$$⊢Q=P\cup \left\{⟨x,G\left(Z\right)⟩\right\}$$
	bnj1312.13	$$⊢W=⟨z,{Q\upharpoonright }_{pred\left(z,A,R\right)}⟩$$
	bnj1312.14	$$⊢E=\left\{x\right\}\cup trCl\left(x,A,R\right)$$
Assertion	bnj1312	$$⊢RFrSeA\to \forall x\in A\exists f\in C\mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)$$

Proof

Step	Hyp	Ref	Expression
1		bnj1312.1	$$⊢B=\left\{d|\left(d\subseteq A\wedge \forall x\in dpred\left(x,A,R\right)\subseteq d\right)\right\}$$
2		bnj1312.2	$$⊢Y=⟨x,{f\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
3		bnj1312.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		bnj1312.4	$$⊢\tau \leftrightarrow \left(f\in C\wedge \mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
5		bnj1312.5	$$⊢D=\left\{x\in A|\neg \exists f\tau \right\}$$
6		bnj1312.6	$$⊢\psi \leftrightarrow \left(RFrSeA\wedge D\ne \varnothing \right)$$
7		bnj1312.7	$$⊢\chi \leftrightarrow \left(\psi \wedge x\in D\wedge \forall y\in D\neg yRx\right)$$
8		bnj1312.8	Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9		bnj1312.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		bnj1312.10	$$⊢P=\bigcup H$$
11		bnj1312.11	$$⊢Z=⟨x,{P\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
12		bnj1312.12	$$⊢Q=P\cup \left\{⟨x,G\left(Z\right)⟩\right\}$$
13		bnj1312.13	$$⊢W=⟨z,{Q\upharpoonright }_{pred\left(z,A,R\right)}⟩$$
14		bnj1312.14	$$⊢E=\left\{x\right\}\cup trCl\left(x,A,R\right)$$
15	6	simplbi	$$⊢\psi \to RFrSeA$$
16	5	ssrab3	$$⊢D\subseteq A$$
17	16	a1i	$$⊢\psi \to D\subseteq A$$
18	6	simprbi	$$⊢\psi \to D\ne \varnothing$$
19	5	bnj1230	$$⊢w\in D\to \forall xw\in D$$
20	19	bnj1228	$$⊢\left(RFrSeA\wedge D\subseteq A\wedge D\ne \varnothing \right)\to \exists x\in D\forall y\in D\neg yRx$$
21	15 17 18 20	syl3anc	$$⊢\psi \to \exists x\in D\forall y\in D\neg yRx$$
22		nfv	$$⊢ℲxRFrSeA$$
23	19	nfcii	$$⊢\underset{\_}{Ⅎ}xD$$
24		nfcv	$$⊢\underset{\_}{Ⅎ}x\varnothing$$
25	23 24	nfne	$$⊢ℲxD\ne \varnothing$$
26	22 25	nfan	$$⊢Ⅎx\left(RFrSeA\wedge D\ne \varnothing \right)$$
27	6 26	nfxfr	$$⊢Ⅎx\psi$$
28	27	nf5ri	$$⊢\psi \to \forall x\psi$$
29	21 7 28	bnj1521	$$⊢\psi \to \exists x\chi$$
30	7	simp2bi	$$⊢\chi \to x\in D$$
31	5	bnj1538	$$⊢x\in D\to \neg \exists f\tau$$
32	1 2 3 4 5 6 7 8 9 10 11 12	bnj1489	$$⊢\chi \to Q\in \mathrm{V}$$
33	7 15	bnj835	$$⊢\chi \to RFrSeA$$
34	1 2 3 4 5 6 7 8 9 10	bnj1384	$$⊢RFrSeA\to \mathrm{Fun}P$$
35	33 34	syl	$$⊢\chi \to \mathrm{Fun}P$$
36	1 2 3 4 5 6 7 8 9 10	bnj1415	$$⊢\chi \to \mathrm{dom}P=trCl\left(x,A,R\right)$$
37	35 36	bnj1422	$$⊢\chi \to PFntrCl\left(x,A,R\right)$$
38	1 2 3 4 5 6 7 8 9 10 11 12 36	bnj1416	$$⊢\chi \to \mathrm{dom}Q=\left\{x\right\}\cup trCl\left(x,A,R\right)$$
39	1 2 3 4 5 6 7 8 9 10 11 12 35 38 36	bnj1421	$$⊢\chi \to \mathrm{Fun}Q$$
40	39 38	bnj1422	$$⊢\chi \to QFn\left(\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
41	1 2 3 4 5 6 7 8 9 10 11 12 13 14 37 40	bnj1423	$$⊢\chi \to \forall z\in EQ\left(z\right)=G\left(W\right)$$
42	14	fneq2i	$$⊢QFnE\leftrightarrow QFn\left(\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
43	40 42	sylibr	$$⊢\chi \to QFnE$$
44	1 2 3 4 5 6 7 8 9 10 11 12 13 14	bnj1452	$$⊢\chi \to E\in B$$
45	1 2 3 4 5 6 7 8 9 10 11 12 13 14 32 41 43 44	bnj1463	$$⊢\chi \to Q\in C$$
46	45 38	jca	$$⊢\chi \to \left(Q\in C\wedge \mathrm{dom}Q=\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
47	1 2 3 4 5 6 7 8 9 10 11 12 46	bnj1491	$$⊢\left(\chi \wedge Q\in \mathrm{V}\right)\to \exists f\left(f\in C\wedge \mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
48	32 47	mpdan	$$⊢\chi \to \exists f\left(f\in C\wedge \mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
49	48 4	bnj1198	$$⊢\chi \to \exists f\tau$$
50	31 49	nsyl3	$$⊢\chi \to \neg x\in D$$
51	29 30 50	bnj1304	$$⊢\neg \psi$$
52	6 51	bnj1541	$$⊢RFrSeA\to D=\varnothing$$
53	5 52	bnj1476	$$⊢RFrSeA\to \forall x\in A\exists f\tau$$
54	4	exbii	$$⊢\exists f\tau \leftrightarrow \exists f\left(f\in C\wedge \mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
55		df-rex	$$⊢\exists f\in C\mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)\leftrightarrow \exists f\left(f\in C\wedge \mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
56	54 55	bitr4i	$$⊢\exists f\tau \leftrightarrow \exists f\in C\mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)$$
57	56	ralbii	$$⊢\forall x\in A\exists f\tau \leftrightarrow \forall x\in A\exists f\in C\mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)$$
58	53 57	sylib	$$⊢RFrSeA\to \forall x\in A\exists f\in C\mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)$$