Theorem bnj1371

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

Proof

Step	Hyp	Ref	Expression
1		bnj1371.1	$$⊢B=\left\{d|\left(d\subseteq A\wedge \forall x\in dpred\left(x,A,R\right)\subseteq d\right)\right\}$$
2		bnj1371.2	$$⊢Y=⟨x,{f\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
3		bnj1371.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		bnj1371.4	$$⊢\tau \leftrightarrow \left(f\in C\wedge \mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
5		bnj1371.5	$$⊢D=\left\{x\in A|\neg \exists f\tau \right\}$$
6		bnj1371.6	$$⊢\psi \leftrightarrow \left(RFrSeA\wedge D\ne \varnothing \right)$$
7		bnj1371.7	$$⊢\chi \leftrightarrow \left(\psi \wedge x\in D\wedge \forall y\in D\neg yRx\right)$$
8		bnj1371.8	Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9		bnj1371.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		bnj1371.10	$$⊢P=\bigcup H$$
11		bnj1371.11	Could not format ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) : No typesetting found for |- ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) with typecode |-
12	9	bnj1436	Could not format ( f e. H -> E. y e. _pred ( x , A , R ) ta' ) : No typesetting found for |- ( f e. H -> E. y e. _pred ( x , A , R ) ta' ) with typecode |-
13		rexex	Could not format ( E. y e. _pred ( x , A , R ) ta' -> E. y ta' ) : No typesetting found for |- ( E. y e. _pred ( x , A , R ) ta' -> E. y ta' ) with typecode |-
14	12 13	syl	Could not format ( f e. H -> E. y ta' ) : No typesetting found for |- ( f e. H -> E. y ta' ) with typecode |-
15	11	exbii	Could not format ( E. y ta' <-> E. y ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) : No typesetting found for |- ( E. y ta' <-> E. y ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) with typecode |-
16	14 15	sylib	$$⊢f\in H\to \exists y\left(f\in C\wedge \mathrm{dom}f=\left\{y\right\}\cup trCl\left(y,A,R\right)\right)$$
17		exsimpl	$$⊢\exists y\left(f\in C\wedge \mathrm{dom}f=\left\{y\right\}\cup trCl\left(y,A,R\right)\right)\to \exists yf\in C$$
18	16 17	syl	$$⊢f\in H\to \exists yf\in C$$
19	3	eqabri	$$⊢f\in C\leftrightarrow \exists d\in B\left(fFnd\wedge \forall x\in df\left(x\right)=G\left(Y\right)\right)$$
20	19	bnj1238	$$⊢f\in C\to \exists d\in BfFnd$$
21		fnfun	$$⊢fFnd\to \mathrm{Fun}f$$
22	20 21	bnj31	$$⊢f\in C\to \exists d\in B\mathrm{Fun}f$$
23	22	bnj1265	$$⊢f\in C\to \mathrm{Fun}f$$
24	18 23	bnj593	$$⊢f\in H\to \exists y\mathrm{Fun}f$$
25	24	bnj937	$$⊢f\in H\to \mathrm{Fun}f$$