This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )