Theorem bnj1421

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

Proof

Step	Hyp	Ref	Expression
1		bnj1421.1	$$⊢B=\left\{d|\left(d\subseteq A\wedge \forall x\in dpred\left(x,A,R\right)\subseteq d\right)\right\}$$
2		bnj1421.2	$$⊢Y=⟨x,{f\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
3		bnj1421.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		bnj1421.4	$$⊢\tau \leftrightarrow \left(f\in C\wedge \mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
5		bnj1421.5	$$⊢D=\left\{x\in A|\neg \exists f\tau \right\}$$
6		bnj1421.6	$$⊢\psi \leftrightarrow \left(RFrSeA\wedge D\ne \varnothing \right)$$
7		bnj1421.7	$$⊢\chi \leftrightarrow \left(\psi \wedge x\in D\wedge \forall y\in D\neg yRx\right)$$
8		bnj1421.8	Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9		bnj1421.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		bnj1421.10	$$⊢P=\bigcup H$$
11		bnj1421.11	$$⊢Z=⟨x,{P\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
12		bnj1421.12	$$⊢Q=P\cup \left\{⟨x,G\left(Z\right)⟩\right\}$$
13		bnj1421.13	$$⊢\chi \to \mathrm{Fun}P$$
14		bnj1421.14	$$⊢\chi \to \mathrm{dom}Q=\left\{x\right\}\cup trCl\left(x,A,R\right)$$
15		bnj1421.15	$$⊢\chi \to \mathrm{dom}P=trCl\left(x,A,R\right)$$
16		vex	$$⊢x\in \mathrm{V}$$
17		fvex	$$⊢G\left(Z\right)\in \mathrm{V}$$
18	16 17	funsn	$$⊢\mathrm{Fun}\left\{⟨x,G\left(Z\right)⟩\right\}$$
19	13 18	jctir	$$⊢\chi \to \left(\mathrm{Fun}P\wedge \mathrm{Fun}\left\{⟨x,G\left(Z\right)⟩\right\}\right)$$
20	17	dmsnop	$$⊢\mathrm{dom}\left\{⟨x,G\left(Z\right)⟩\right\}=\left\{x\right\}$$
21	20	a1i	$$⊢\chi \to \mathrm{dom}\left\{⟨x,G\left(Z\right)⟩\right\}=\left\{x\right\}$$
22	15 21	ineq12d	$$⊢\chi \to \mathrm{dom}P\cap \mathrm{dom}\left\{⟨x,G\left(Z\right)⟩\right\}=trCl\left(x,A,R\right)\cap \left\{x\right\}$$
23	6	simplbi	$$⊢\psi \to RFrSeA$$
24	7 23	bnj835	$$⊢\chi \to RFrSeA$$
25		biid	$$⊢RFrSeA\leftrightarrow RFrSeA$$
26		biid	$$⊢\neg x\in trCl\left(x,A,R\right)\leftrightarrow \neg x\in trCl\left(x,A,R\right)$$
27		biid	$$⊢\forall z\in A\left(zRx\to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\neg x\in trCl\left(x,A,R\right)\right)\leftrightarrow \forall z\in A\left(zRx\to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\neg x\in trCl\left(x,A,R\right)\right)$$
28		biid	$$⊢\left(RFrSeA\wedge x\in A\wedge \forall z\in A\left(zRx\to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\neg x\in trCl\left(x,A,R\right)\right)\right)\leftrightarrow \left(RFrSeA\wedge x\in A\wedge \forall z\in A\left(zRx\to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\neg x\in trCl\left(x,A,R\right)\right)\right)$$
29		eqid	$$⊢pred\left(x,A,R\right)\cup \bigcup _{z\in pred\left(x,A,R\right)}trCl\left(z,A,R\right)=pred\left(x,A,R\right)\cup \bigcup _{z\in pred\left(x,A,R\right)}trCl\left(z,A,R\right)$$
30	25 26 27 28 29	bnj1417	$$⊢RFrSeA\to \forall x\in A\neg x\in trCl\left(x,A,R\right)$$
31		disjsn	$$⊢trCl\left(x,A,R\right)\cap \left\{x\right\}=\varnothing \leftrightarrow \neg x\in trCl\left(x,A,R\right)$$
32	31	ralbii	$$⊢\forall x\in AtrCl\left(x,A,R\right)\cap \left\{x\right\}=\varnothing \leftrightarrow \forall x\in A\neg x\in trCl\left(x,A,R\right)$$
33	30 32	sylibr	$$⊢RFrSeA\to \forall x\in AtrCl\left(x,A,R\right)\cap \left\{x\right\}=\varnothing$$
34	24 33	syl	$$⊢\chi \to \forall x\in AtrCl\left(x,A,R\right)\cap \left\{x\right\}=\varnothing$$
35	5 7	bnj1212	$$⊢\chi \to x\in A$$
36	34 35	bnj1294	$$⊢\chi \to trCl\left(x,A,R\right)\cap \left\{x\right\}=\varnothing$$
37	22 36	eqtrd	$$⊢\chi \to \mathrm{dom}P\cap \mathrm{dom}\left\{⟨x,G\left(Z\right)⟩\right\}=\varnothing$$
38		funun	$$⊢\left(\left(\mathrm{Fun}P\wedge \mathrm{Fun}\left\{⟨x,G\left(Z\right)⟩\right\}\right)\wedge \mathrm{dom}P\cap \mathrm{dom}\left\{⟨x,G\left(Z\right)⟩\right\}=\varnothing \right)\to \mathrm{Fun}\left(P\cup \left\{⟨x,G\left(Z\right)⟩\right\}\right)$$
39	19 37 38	syl2anc	$$⊢\chi \to \mathrm{Fun}\left(P\cup \left\{⟨x,G\left(Z\right)⟩\right\}\right)$$
40	12	funeqi	$$⊢\mathrm{Fun}Q\leftrightarrow \mathrm{Fun}\left(P\cup \left\{⟨x,G\left(Z\right)⟩\right\}\right)$$
41	39 40	sylibr	$$⊢\chi \to \mathrm{Fun}Q$$