Theorem bnj1489

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

Proof

Step	Hyp	Ref	Expression
1		bnj1489.1	$$⊢B=\left\{d|\left(d\subseteq A\wedge \forall x\in dpred\left(x,A,R\right)\subseteq d\right)\right\}$$
2		bnj1489.2	$$⊢Y=⟨x,{f\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
3		bnj1489.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		bnj1489.4	$$⊢\tau \leftrightarrow \left(f\in C\wedge \mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
5		bnj1489.5	$$⊢D=\left\{x\in A|\neg \exists f\tau \right\}$$
6		bnj1489.6	$$⊢\psi \leftrightarrow \left(RFrSeA\wedge D\ne \varnothing \right)$$
7		bnj1489.7	$$⊢\chi \leftrightarrow \left(\psi \wedge x\in D\wedge \forall y\in D\neg yRx\right)$$
8		bnj1489.8	Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9		bnj1489.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		bnj1489.10	$$⊢P=\bigcup H$$
11		bnj1489.11	$$⊢Z=⟨x,{P\upharpoonright }_{pred\left(x,A,R\right)}⟩$$
12		bnj1489.12	$$⊢Q=P\cup \left\{⟨x,G\left(Z\right)⟩\right\}$$
13		bnj1364	$$⊢RFrSeA\to RSeA$$
14		df-bnj13	$$⊢RSeA\leftrightarrow \forall x\in Apred\left(x,A,R\right)\in \mathrm{V}$$
15	13 14	sylib	$$⊢RFrSeA\to \forall x\in Apred\left(x,A,R\right)\in \mathrm{V}$$
16	6 15	bnj832	$$⊢\psi \to \forall x\in Apred\left(x,A,R\right)\in \mathrm{V}$$
17	7 16	bnj835	$$⊢\chi \to \forall x\in Apred\left(x,A,R\right)\in \mathrm{V}$$
18	5 7	bnj1212	$$⊢\chi \to x\in A$$
19	17 18	bnj1294	$$⊢\chi \to pred\left(x,A,R\right)\in \mathrm{V}$$
20		nfv	$$⊢Ⅎy\psi$$
21		nfv	$$⊢Ⅎyx\in D$$
22		nfra1	$$⊢Ⅎy\forall y\in D\neg yRx$$
23	20 21 22	nf3an	$$⊢Ⅎy\left(\psi \wedge x\in D\wedge \forall y\in D\neg yRx\right)$$
24	7 23	nfxfr	$$⊢Ⅎy\chi$$
25	6	simplbi	$$⊢\psi \to RFrSeA$$
26	7 25	bnj835	$$⊢\chi \to RFrSeA$$
27	26	adantr	$$⊢\left(\chi \wedge y\in pred\left(x,A,R\right)\right)\to RFrSeA$$
28	1 2 3 4 5 6 7 8	bnj1388	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 |-
29	28	r19.21bi	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 |-
30		nfv	$$⊢ℲxRFrSeA$$
31		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\tau$$
32	8 31	nfxfr	Could not format F/ x ta' : No typesetting found for |- F/ x ta' with typecode |-
33	32	nfex	Could not format F/ x E. f ta' : No typesetting found for |- F/ x E. f ta' with typecode |-
34	30 33	nfan	Could not format F/ x ( R _FrSe A /\ E. f ta' ) : No typesetting found for |- F/ x ( R _FrSe A /\ E. f ta' ) with typecode |-
35	32	nfeuw	Could not format F/ x E! f ta' : No typesetting found for |- F/ x E! f ta' with typecode |-
36	34 35	nfim	Could not format F/ x ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) : No typesetting found for |- F/ x ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) with typecode |-
37		sneq	$$⊢x=y\to \left\{x\right\}=\left\{y\right\}$$
38		bnj1318	$$⊢x=y\to trCl\left(x,A,R\right)=trCl\left(y,A,R\right)$$
39	37 38	uneq12d	$$⊢x=y\to \left\{x\right\}\cup trCl\left(x,A,R\right)=\left\{y\right\}\cup trCl\left(y,A,R\right)$$
40	39	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)$$
41	40	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)$$
42	1 2 3 4 8	bnj1373	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 |-
43	41 42	bitr4di	Could not format ( x = y -> ( ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> ta' ) ) : No typesetting found for |- ( x = y -> ( ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> ta' ) ) with typecode |-
44	43	exbidv	Could not format ( x = y -> ( E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> E. f ta' ) ) : No typesetting found for |- ( x = y -> ( E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> E. f ta' ) ) with typecode |-
45	44	anbi2d	Could not format ( x = y -> ( ( R _FrSe A /\ E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) <-> ( R _FrSe A /\ E. f ta' ) ) ) : No typesetting found for |- ( x = y -> ( ( R _FrSe A /\ E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) <-> ( R _FrSe A /\ E. f ta' ) ) ) with typecode |-
46	43	eubidv	Could not format ( x = y -> ( E! f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> E! f ta' ) ) : No typesetting found for |- ( x = y -> ( E! f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> E! f ta' ) ) with typecode |-
47	45 46	imbi12d	Could not format ( x = y -> ( ( ( R _FrSe A /\ E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) -> E! f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) <-> ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) ) ) : No typesetting found for |- ( x = y -> ( ( ( R _FrSe A /\ E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) -> E! f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) <-> ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) ) ) with typecode |-
48		biid	$$⊢\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\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
49	1 2 3 48	bnj1321	$$⊢\left(RFrSeA\wedge \exists f\left(f\in C\wedge \mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)\right)\right)\to \exists !f\left(f\in C\wedge \mathrm{dom}f=\left\{x\right\}\cup trCl\left(x,A,R\right)\right)$$
50	36 47 49	chvarfv	Could not format ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) : No typesetting found for |- ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) with typecode |-
51	27 29 50	syl2anc	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 |-
52	51	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 |-
53	24 52	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 |-
54	9	a1i	Could not format ( ch -> H = { f | E. y e. _pred ( x , A , R ) ta' } ) : No typesetting found for |- ( ch -> H = { f | E. y e. _pred ( x , A , R ) ta' } ) with typecode |-
55		biid	Could not format ( ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. _pred ( x , A , R ) ta' } ) <-> ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. _pred ( x , A , R ) ta' } ) ) : No typesetting found for |- ( ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. _pred ( x , A , R ) ta' } ) <-> ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. _pred ( x , A , R ) ta' } ) ) with typecode |-
56	55	bnj1366	Could not format ( ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. _pred ( x , A , R ) ta' } ) -> H e. _V ) : No typesetting found for |- ( ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. _pred ( x , A , R ) ta' } ) -> H e. _V ) with typecode |-
57	19 53 54 56	syl3anc	$$⊢\chi \to H\in \mathrm{V}$$
58	57	uniexd	$$⊢\chi \to \bigcup H\in \mathrm{V}$$
59	10 58	eqeltrid	$$⊢\chi \to P\in \mathrm{V}$$
60		snex	$$⊢\left\{⟨x,G\left(Z\right)⟩\right\}\in \mathrm{V}$$
61	60	a1i	$$⊢\chi \to \left\{⟨x,G\left(Z\right)⟩\right\}\in \mathrm{V}$$
62	59 61	bnj1149	$$⊢\chi \to P\cup \left\{⟨x,G\left(Z\right)⟩\right\}\in \mathrm{V}$$
63	12 62	eqeltrid	$$⊢\chi \to Q\in \mathrm{V}$$