Theorem bnj1373

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	bnj1373.1	$$⊢B=\left\{d|\left(d\subseteq A\wedge \forall x\in dpred\left(x,A,R\right)\subseteq d\right)\right\}$$
	bnj1373.2	$$⊢Y=⟨x,{f\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
	bnj1373.3	$$⊢C=\left\{f|\exists d\in B\left(fFnd\wedge \forall x\in df\left(x\right)=G\left(Y\right)\right)\right\}$$
	bnj1373.4	$$⊢\tau \leftrightarrow \left(f\in C\wedge \mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
	bnj1373.5	No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
Assertion	bnj1373	Could not format assertion : No typesetting found for |- ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bnj1373.1	$$⊢B=\left\{d|\left(d\subseteq A\wedge \forall x\in dpred\left(x,A,R\right)\subseteq d\right)\right\}$$
2		bnj1373.2	$$⊢Y=⟨x,{f\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
3		bnj1373.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		bnj1373.4	$$⊢\tau \leftrightarrow \left(f\in C\wedge \mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
5		bnj1373.5	Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
6	1	bnj1309	$$⊢f\in B\to \forall xf\in B$$
7	3 6	bnj1307	$$⊢f\in C\to \forall xf\in C$$
8	7	bnj1351	$$⊢\left(f\in C\wedge \mathrm{dom}f=\left\{y\right\}\cup trCl\left(y,A,R\right)\right)\to \forall x\left(f\in C\wedge \mathrm{dom}f=\left\{y\right\}\cup trCl\left(y,A,R\right)\right)$$
9	8	nf5i	$$⊢Ⅎx\left(f\in C\wedge \mathrm{dom}f=\left\{y\right\}\cup trCl\left(y,A,R\right)\right)$$
10		sneq	$$⊢x=y\to \left\{x\right\}=\left\{y\right\}$$
11		bnj1318	$$⊢x=y\to trCl\left(x,A,R\right)=trCl\left(y,A,R\right)$$
12	10 11	uneq12d	$$⊢x=y\to \left\{x\right\}\cup trCl\left(x,A,R\right)=\left\{y\right\}\cup trCl\left(y,A,R\right)$$
13	12	eqeq2d	$$⊢x=y\to \left(\mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)\leftrightarrow \mathrm{dom}f=\left\{y\right\}\cup trCl\left(y,A,R\right)\right)$$
14	13	anbi2d	$$⊢x=y\to \left(\left(f\in C\wedge \mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)\right)\leftrightarrow \left(f\in C\wedge \mathrm{dom}f=\left\{y\right\}\cup trCl\left(y,A,R\right)\right)\right)$$
15	4 14	syl5bb	$$⊢x=y\to \left(\tau \leftrightarrow \left(f\in C\wedge \mathrm{dom}f=\left\{y\right\}\cup trCl\left(y,A,R\right)\right)\right)$$
16	9 15	sbciegf	$$⊢y\in \mathrm{V}\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\tau \leftrightarrow \left(f\in C\wedge \mathrm{dom}f=\left\{y\right\}\cup trCl\left(y,A,R\right)\right)\right)$$
17	16	elv	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\tau \leftrightarrow \left(f\in C\wedge \mathrm{dom}f=\left\{y\right\}\cup trCl\left(y,A,R\right)\right)$$
18	5 17	bitri	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 |-