Theorem bnj1519

Description: Technical lemma for bnj1500 . 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	bnj1519.1	|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
	bnj1519.2	|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
	bnj1519.3	|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
	bnj1519.4	|- F = U. C
Assertion	bnj1519	|- ( ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) -> A. d ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) )

Proof

Step	Hyp	Ref	Expression
1		bnj1519.1	|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2		bnj1519.2	|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
3		bnj1519.3	|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4		bnj1519.4	|- F = U. C
5		nfre1	|- F/ d E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) )
6	5	nfab	|- F/_ d { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
7	3 6	nfcxfr	|- F/_ d C
8	7	nfuni	|- F/_ d U. C
9	4 8	nfcxfr	|- F/_ d F
10		nfcv	|- F/_ d x
11	9 10	nffv	|- F/_ d ( F ` x )
12		nfcv	|- F/_ d G
13		nfcv	|- F/_ d _pred ( x , A , R )
14	9 13	nfres	|- F/_ d ( F |` _pred ( x , A , R ) )
15	10 14	nfop	|- F/_ d <. x , ( F |` _pred ( x , A , R ) ) >.
16	12 15	nffv	|- F/_ d ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. )
17	11 16	nfeq	|- F/ d ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. )
18	17	nf5ri	|- ( ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) -> A. d ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) )