Theorem bnj1466

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	bnj1466.1	|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
	bnj1466.2	|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
	bnj1466.3	|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
	bnj1466.4	|- ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) )
	bnj1466.5	|- D = { x e. A | -. E. f ta }
	bnj1466.6	|- ( ps <-> ( R _FrSe A /\ D =/= (/) ) )
	bnj1466.7	|- ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) )
	bnj1466.8	|- ( ta' <-> [. y / x ]. ta )
	bnj1466.9	|- H = { f | E. y e. _pred ( x , A , R ) ta' }
	bnj1466.10	|- P = U. H
	bnj1466.11	|- Z = <. x , ( P |` _pred ( x , A , R ) ) >.
	bnj1466.12	|- Q = ( P u. { <. x , ( G ` Z ) >. } )
Assertion	bnj1466	|- ( w e. Q -> A. f w e. Q )

Proof

Step	Hyp	Ref	Expression
1		bnj1466.1	|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2		bnj1466.2	|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
3		bnj1466.3	|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4		bnj1466.4	|- ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) )
5		bnj1466.5	|- D = { x e. A | -. E. f ta }
6		bnj1466.6	|- ( ps <-> ( R _FrSe A /\ D =/= (/) ) )
7		bnj1466.7	|- ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) )
8		bnj1466.8	|- ( ta' <-> [. y / x ]. ta )
9		bnj1466.9	|- H = { f | E. y e. _pred ( x , A , R ) ta' }
10		bnj1466.10	|- P = U. H
11		bnj1466.11	|- Z = <. x , ( P |` _pred ( x , A , R ) ) >.
12		bnj1466.12	|- Q = ( P u. { <. x , ( G ` Z ) >. } )
13	9	bnj1317	|- ( w e. H -> A. f w e. H )
14	13	nfcii	|- F/_ f H
15	14	nfuni	|- F/_ f U. H
16	10 15	nfcxfr	|- F/_ f P
17		nfcv	|- F/_ f x
18		nfcv	|- F/_ f G
19		nfcv	|- F/_ f _pred ( x , A , R )
20	16 19	nfres	|- F/_ f ( P |` _pred ( x , A , R ) )
21	17 20	nfop	|- F/_ f <. x , ( P |` _pred ( x , A , R ) ) >.
22	11 21	nfcxfr	|- F/_ f Z
23	18 22	nffv	|- F/_ f ( G ` Z )
24	17 23	nfop	|- F/_ f <. x , ( G ` Z ) >.
25	24	nfsn	|- F/_ f { <. x , ( G ` Z ) >. }
26	16 25	nfun	|- F/_ f ( P u. { <. x , ( G ` Z ) >. } )
27	12 26	nfcxfr	|- F/_ f Q
28	27	nfcrii	|- ( w e. Q -> A. f w e. Q )