Theorem bnj66

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

Proof

Step	Hyp	Ref	Expression
1		bnj66.1	|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2		bnj66.2	|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
3		bnj66.3	|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4		fneq1	|- ( g = f -> ( g Fn d <-> f Fn d ) )
5		fveq1	|- ( g = f -> ( g ` x ) = ( f ` x ) )
6		reseq1	|- ( g = f -> ( g |` _pred ( x , A , R ) ) = ( f |` _pred ( x , A , R ) ) )
7	6	opeq2d	|- ( g = f -> <. x , ( g |` _pred ( x , A , R ) ) >. = <. x , ( f |` _pred ( x , A , R ) ) >. )
8	7 2	eqtr4di	|- ( g = f -> <. x , ( g |` _pred ( x , A , R ) ) >. = Y )
9	8	fveq2d	|- ( g = f -> ( G ` <. x , ( g |` _pred ( x , A , R ) ) >. ) = ( G ` Y ) )
10	5 9	eqeq12d	|- ( g = f -> ( ( g ` x ) = ( G ` <. x , ( g |` _pred ( x , A , R ) ) >. ) <-> ( f ` x ) = ( G ` Y ) ) )
11	10	ralbidv	|- ( g = f -> ( A. x e. d ( g ` x ) = ( G ` <. x , ( g |` _pred ( x , A , R ) ) >. ) <-> A. x e. d ( f ` x ) = ( G ` Y ) ) )
12	4 11	anbi12d	|- ( g = f -> ( ( g Fn d /\ A. x e. d ( g ` x ) = ( G ` <. x , ( g |` _pred ( x , A , R ) ) >. ) ) <-> ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) ) )
13	12	rexbidv	|- ( g = f -> ( E. d e. B ( g Fn d /\ A. x e. d ( g ` x ) = ( G ` <. x , ( g |` _pred ( x , A , R ) ) >. ) ) <-> E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) ) )
14	13	cbvabv	|- { g | E. d e. B ( g Fn d /\ A. x e. d ( g ` x ) = ( G ` <. x , ( g |` _pred ( x , A , R ) ) >. ) ) } = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
15	3 14	eqtr4i	|- C = { g | E. d e. B ( g Fn d /\ A. x e. d ( g ` x ) = ( G ` <. x , ( g |` _pred ( x , A , R ) ) >. ) ) }
16	15	bnj1436	|- ( g e. C -> E. d e. B ( g Fn d /\ A. x e. d ( g ` x ) = ( G ` <. x , ( g |` _pred ( x , A , R ) ) >. ) ) )
17		bnj1239	|- ( E. d e. B ( g Fn d /\ A. x e. d ( g ` x ) = ( G ` <. x , ( g |` _pred ( x , A , R ) ) >. ) ) -> E. d e. B g Fn d )
18		fnrel	|- ( g Fn d -> Rel g )
19	18	rexlimivw	|- ( E. d e. B g Fn d -> Rel g )
20	16 17 19	3syl	|- ( g e. C -> Rel g )