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 ) ) >. ) )

Metamath Proof Explorer

Theorem bnj1519

Proof