Metamath Proof Explorer

Theorem bnj1529

Description: Technical lemma for bnj1522 . 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 bnj1529.1 
|- ( ch -> A. x e. A ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) )
bnj1529.2 
|- ( w e. F -> A. x w e. F )
Assertion bnj1529 
|- ( ch -> A. y e. A ( F ` y ) = ( G ` <. y , ( F |` _pred ( y , A , R ) ) >. ) )

Proof

Step Hyp Ref Expression
1 bnj1529.1 
 |-  ( ch -> A. x e. A ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) )
2 bnj1529.2 
 |-  ( w e. F -> A. x w e. F )
3 nfv 
 |-  F/ y ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. )
4 2 nfcii 
 |-  F/_ x F
5 nfcv 
 |-  F/_ x y
6 4 5 nffv 
 |-  F/_ x ( F ` y )
7 nfcv 
 |-  F/_ x G
8 nfcv 
 |-  F/_ x _pred ( y , A , R )
9 4 8 nfres 
 |-  F/_ x ( F |` _pred ( y , A , R ) )
10 5 9 nfop 
 |-  F/_ x <. y , ( F |` _pred ( y , A , R ) ) >.
11 7 10 nffv 
 |-  F/_ x ( G ` <. y , ( F |` _pred ( y , A , R ) ) >. )
12 6 11 nfeq 
 |-  F/ x ( F ` y ) = ( G ` <. y , ( F |` _pred ( y , A , R ) ) >. )
13 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
14 id 
 |-  ( x = y -> x = y )
15 bnj602 
 |-  ( x = y -> _pred ( x , A , R ) = _pred ( y , A , R ) )
16 15 reseq2d 
 |-  ( x = y -> ( F |` _pred ( x , A , R ) ) = ( F |` _pred ( y , A , R ) ) )
17 14 16 opeq12d 
 |-  ( x = y -> <. x , ( F |` _pred ( x , A , R ) ) >. = <. y , ( F |` _pred ( y , A , R ) ) >. )
18 17 fveq2d 
 |-  ( x = y -> ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) = ( G ` <. y , ( F |` _pred ( y , A , R ) ) >. ) )
19 13 18 eqeq12d 
 |-  ( x = y -> ( ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) <-> ( F ` y ) = ( G ` <. y , ( F |` _pred ( y , A , R ) ) >. ) ) )
20 3 12 19 cbvralw 
 |-  ( A. x e. A ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) <-> A. y e. A ( F ` y ) = ( G ` <. y , ( F |` _pred ( y , A , R ) ) >. ) )
21 1 20 sylib 
 |-  ( ch -> A. y e. A ( F ` y ) = ( G ` <. y , ( F |` _pred ( y , A , R ) ) >. ) )