Metamath Proof Explorer

Theorem bnj1326

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 bnj1326.1 
|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
bnj1326.2 
|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
bnj1326.3 
|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
bnj1326.4 
|- D = ( dom g i^i dom h )
Assertion bnj1326 
|- ( ( R _FrSe A /\ g e. C /\ h e. C ) -> ( g |` D ) = ( h |` D ) )

Proof

Step Hyp Ref Expression
1 bnj1326.1 
 |-  B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2 bnj1326.2 
 |-  Y = <. x , ( f |` _pred ( x , A , R ) ) >.
3 bnj1326.3 
 |-  C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4 bnj1326.4 
 |-  D = ( dom g i^i dom h )
5 eleq1w 
 |-  ( q = h -> ( q e. C <-> h e. C ) )
6 5 3anbi3d 
 |-  ( q = h -> ( ( R _FrSe A /\ g e. C /\ q e. C ) <-> ( R _FrSe A /\ g e. C /\ h e. C ) ) )
7 dmeq 
 |-  ( q = h -> dom q = dom h )
8 7 ineq2d 
 |-  ( q = h -> ( dom g i^i dom q ) = ( dom g i^i dom h ) )
9 8 reseq2d 
 |-  ( q = h -> ( g |` ( dom g i^i dom q ) ) = ( g |` ( dom g i^i dom h ) ) )
10 4 reseq2i 
 |-  ( g |` D ) = ( g |` ( dom g i^i dom h ) )
11 9 10 eqtr4di 
 |-  ( q = h -> ( g |` ( dom g i^i dom q ) ) = ( g |` D ) )
12 8 reseq2d 
 |-  ( q = h -> ( q |` ( dom g i^i dom q ) ) = ( q |` ( dom g i^i dom h ) ) )
13 reseq1 
 |-  ( q = h -> ( q |` ( dom g i^i dom h ) ) = ( h |` ( dom g i^i dom h ) ) )
14 12 13 eqtrd 
 |-  ( q = h -> ( q |` ( dom g i^i dom q ) ) = ( h |` ( dom g i^i dom h ) ) )
15 4 reseq2i 
 |-  ( h |` D ) = ( h |` ( dom g i^i dom h ) )
16 14 15 eqtr4di 
 |-  ( q = h -> ( q |` ( dom g i^i dom q ) ) = ( h |` D ) )
17 11 16 eqeq12d 
 |-  ( q = h -> ( ( g |` ( dom g i^i dom q ) ) = ( q |` ( dom g i^i dom q ) ) <-> ( g |` D ) = ( h |` D ) ) )
18 6 17 imbi12d 
 |-  ( q = h -> ( ( ( R _FrSe A /\ g e. C /\ q e. C ) -> ( g |` ( dom g i^i dom q ) ) = ( q |` ( dom g i^i dom q ) ) ) <-> ( ( R _FrSe A /\ g e. C /\ h e. C ) -> ( g |` D ) = ( h |` D ) ) ) )
19 eleq1w 
 |-  ( p = g -> ( p e. C <-> g e. C ) )
20 19 3anbi2d 
 |-  ( p = g -> ( ( R _FrSe A /\ p e. C /\ q e. C ) <-> ( R _FrSe A /\ g e. C /\ q e. C ) ) )
21 dmeq 
 |-  ( p = g -> dom p = dom g )
22 21 ineq1d 
 |-  ( p = g -> ( dom p i^i dom q ) = ( dom g i^i dom q ) )
23 22 reseq2d 
 |-  ( p = g -> ( p |` ( dom p i^i dom q ) ) = ( p |` ( dom g i^i dom q ) ) )
24 reseq1 
 |-  ( p = g -> ( p |` ( dom g i^i dom q ) ) = ( g |` ( dom g i^i dom q ) ) )
25 23 24 eqtrd 
 |-  ( p = g -> ( p |` ( dom p i^i dom q ) ) = ( g |` ( dom g i^i dom q ) ) )
26 22 reseq2d 
 |-  ( p = g -> ( q |` ( dom p i^i dom q ) ) = ( q |` ( dom g i^i dom q ) ) )
27 25 26 eqeq12d 
 |-  ( p = g -> ( ( p |` ( dom p i^i dom q ) ) = ( q |` ( dom p i^i dom q ) ) <-> ( g |` ( dom g i^i dom q ) ) = ( q |` ( dom g i^i dom q ) ) ) )
28 20 27 imbi12d 
 |-  ( p = g -> ( ( ( R _FrSe A /\ p e. C /\ q e. C ) -> ( p |` ( dom p i^i dom q ) ) = ( q |` ( dom p i^i dom q ) ) ) <-> ( ( R _FrSe A /\ g e. C /\ q e. C ) -> ( g |` ( dom g i^i dom q ) ) = ( q |` ( dom g i^i dom q ) ) ) ) )
29 eqid 
 |-  ( dom p i^i dom q ) = ( dom p i^i dom q )
30 1 2 3 29 bnj1311 
 |-  ( ( R _FrSe A /\ p e. C /\ q e. C ) -> ( p |` ( dom p i^i dom q ) ) = ( q |` ( dom p i^i dom q ) ) )
31 28 30 chvarvv 
 |-  ( ( R _FrSe A /\ g e. C /\ q e. C ) -> ( g |` ( dom g i^i dom q ) ) = ( q |` ( dom g i^i dom q ) ) )
32 18 31 chvarvv 
 |-  ( ( R _FrSe A /\ g e. C /\ h e. C ) -> ( g |` D ) = ( h |` D ) )