Theorem bnj1497

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	bnj1497.1	|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
	bnj1497.2	|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
	bnj1497.3	|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
Assertion	bnj1497	|- A. g e. C Fun g

Proof

Step	Hyp	Ref	Expression
1		bnj1497.1	|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2		bnj1497.2	|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
3		bnj1497.3	|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4	3	bnj1317	|- ( g e. C -> A. f g e. C )
5	4	nf5i	|- F/ f g e. C
6		nfv	|- F/ f Fun g
7	5 6	nfim	|- F/ f ( g e. C -> Fun g )
8		eleq1w	|- ( f = g -> ( f e. C <-> g e. C ) )
9		funeq	|- ( f = g -> ( Fun f <-> Fun g ) )
10	8 9	imbi12d	|- ( f = g -> ( ( f e. C -> Fun f ) <-> ( g e. C -> Fun g ) ) )
11	3	bnj1436	|- ( f e. C -> E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) )
12	11	bnj1299	|- ( f e. C -> E. d e. B f Fn d )
13		fnfun	|- ( f Fn d -> Fun f )
14	12 13	bnj31	|- ( f e. C -> E. d e. B Fun f )
15	14	bnj1265	|- ( f e. C -> Fun f )
16	7 10 15	chvarfv	|- ( g e. C -> Fun g )
17	16	rgen	|- A. g e. C Fun g