Theorem bnj1388

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

Proof

Step	Hyp	Ref	Expression
1		bnj1388.1	$$⊢B=\left\{d|\left(d\subseteq A\wedge \forall x\in dpred\left(x,A,R\right)\subseteq d\right)\right\}$$
2		bnj1388.2	$$⊢Y=⟨x,{f\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
3		bnj1388.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		bnj1388.4	$$⊢\tau \leftrightarrow \left(f\in C\wedge \mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
5		bnj1388.5	$$⊢D=\left\{x\in A|\neg \exists f\tau \right\}$$
6		bnj1388.6	$$⊢\psi \leftrightarrow \left(RFrSeA\wedge D\ne \varnothing \right)$$
7		bnj1388.7	$$⊢\chi \leftrightarrow \left(\psi \wedge x\in D\wedge \forall y\in D\neg yRx\right)$$
8		bnj1388.8	Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9		nfv	$$⊢Ⅎy\psi$$
10		nfv	$$⊢Ⅎyx\in D$$
11		nfra1	$$⊢Ⅎy\forall y\in D\neg yRx$$
12	9 10 11	nf3an	$$⊢Ⅎy\left(\psi \wedge x\in D\wedge \forall y\in D\neg yRx\right)$$
13	7 12	nfxfr	$$⊢Ⅎy\chi$$
14		bnj1152	$$⊢y\in pred\left(x,A,R\right)\leftrightarrow \left(y\in A\wedge yRx\right)$$
15	14	simplbi	$$⊢y\in pred\left(x,A,R\right)\to y\in A$$
16	15	adantl	$$⊢\left(\chi \wedge y\in pred\left(x,A,R\right)\right)\to y\in A$$
17	14	biimpi	$$⊢y\in pred\left(x,A,R\right)\to \left(y\in A\wedge yRx\right)$$
18	17	adantl	$$⊢\left(\chi \wedge y\in pred\left(x,A,R\right)\right)\to \left(y\in A\wedge yRx\right)$$
19	18	simprd	$$⊢\left(\chi \wedge y\in pred\left(x,A,R\right)\right)\to yRx$$
20	7	simp3bi	$$⊢\chi \to \forall y\in D\neg yRx$$
21	20	adantr	$$⊢\left(\chi \wedge y\in pred\left(x,A,R\right)\right)\to \forall y\in D\neg yRx$$
22		df-ral	$$⊢\forall y\in D\neg yRx\leftrightarrow \forall y\left(y\in D\to \neg yRx\right)$$
23		con2b	$$⊢\left(y\in D\to \neg yRx\right)\leftrightarrow \left(yRx\to \neg y\in D\right)$$
24	23	albii	$$⊢\forall y\left(y\in D\to \neg yRx\right)\leftrightarrow \forall y\left(yRx\to \neg y\in D\right)$$
25	22 24	bitri	$$⊢\forall y\in D\neg yRx\leftrightarrow \forall y\left(yRx\to \neg y\in D\right)$$
26		sp	$$⊢\forall y\left(yRx\to \neg y\in D\right)\to \left(yRx\to \neg y\in D\right)$$
27	26	impcom	$$⊢\left(yRx\wedge \forall y\left(yRx\to \neg y\in D\right)\right)\to \neg y\in D$$
28	25 27	sylan2b	$$⊢\left(yRx\wedge \forall y\in D\neg yRx\right)\to \neg y\in D$$
29	19 21 28	syl2anc	$$⊢\left(\chi \wedge y\in pred\left(x,A,R\right)\right)\to \neg y\in D$$
30	5	eleq2i	$$⊢y\in D\leftrightarrow y\in \left\{x\in A|\neg \exists f\tau \right\}$$
31		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
32		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
33		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\tau$$
34	8 33	nfxfr	Could not format F/ x ta' : No typesetting found for |- F/ x ta' with typecode |-
35	34	nfex	Could not format F/ x E. f ta' : No typesetting found for |- F/ x E. f ta' with typecode |-
36	35	nfn	Could not format F/ x -. E. f ta' : No typesetting found for |- F/ x -. E. f ta' with typecode |-
37		sbceq1a	$$⊢x=y\to \left(\tau \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\tau \right)$$
38	37 8	bitr4di	Could not format ( x = y -> ( ta <-> ta' ) ) : No typesetting found for |- ( x = y -> ( ta <-> ta' ) ) with typecode |-
39	38	exbidv	Could not format ( x = y -> ( E. f ta <-> E. f ta' ) ) : No typesetting found for |- ( x = y -> ( E. f ta <-> E. f ta' ) ) with typecode |-
40	39	notbid	Could not format ( x = y -> ( -. E. f ta <-> -. E. f ta' ) ) : No typesetting found for |- ( x = y -> ( -. E. f ta <-> -. E. f ta' ) ) with typecode |-
41	31 32 36 40	elrabf	Could not format ( y e. { x e. A | -. E. f ta } <-> ( y e. A /\ -. E. f ta' ) ) : No typesetting found for |- ( y e. { x e. A | -. E. f ta } <-> ( y e. A /\ -. E. f ta' ) ) with typecode |-
42	30 41	bitri	Could not format ( y e. D <-> ( y e. A /\ -. E. f ta' ) ) : No typesetting found for |- ( y e. D <-> ( y e. A /\ -. E. f ta' ) ) with typecode |-
43	29 42	sylnib	Could not format ( ( ch /\ y e. _pred ( x , A , R ) ) -> -. ( y e. A /\ -. E. f ta' ) ) : No typesetting found for |- ( ( ch /\ y e. _pred ( x , A , R ) ) -> -. ( y e. A /\ -. E. f ta' ) ) with typecode |-
44		iman	Could not format ( ( y e. A -> E. f ta' ) <-> -. ( y e. A /\ -. E. f ta' ) ) : No typesetting found for |- ( ( y e. A -> E. f ta' ) <-> -. ( y e. A /\ -. E. f ta' ) ) with typecode |-
45	43 44	sylibr	Could not format ( ( ch /\ y e. _pred ( x , A , R ) ) -> ( y e. A -> E. f ta' ) ) : No typesetting found for |- ( ( ch /\ y e. _pred ( x , A , R ) ) -> ( y e. A -> E. f ta' ) ) with typecode |-
46	16 45	mpd	Could not format ( ( ch /\ y e. _pred ( x , A , R ) ) -> E. f ta' ) : No typesetting found for |- ( ( ch /\ y e. _pred ( x , A , R ) ) -> E. f ta' ) with typecode |-
47	46	ex	Could not format ( ch -> ( y e. _pred ( x , A , R ) -> E. f ta' ) ) : No typesetting found for |- ( ch -> ( y e. _pred ( x , A , R ) -> E. f ta' ) ) with typecode |-
48	13 47	ralrimi	Could not format ( ch -> A. y e. _pred ( x , A , R ) E. f ta' ) : No typesetting found for |- ( ch -> A. y e. _pred ( x , A , R ) E. f ta' ) with typecode |-