Metamath Proof Explorer

Theorem bnj953

Description: Technical lemma for bnj69 . 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 bnj953.1 
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj953.2 
|- ( ( G ` i ) = ( f ` i ) -> A. y ( G ` i ) = ( f ` i ) )
Assertion bnj953 
|- ( ( ( G ` i ) = ( f ` i ) /\ ( G ` suc i ) = ( f ` suc i ) /\ ( i e. _om /\ suc i e. n ) /\ ps ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) )

Proof

Step Hyp Ref Expression
1 bnj953.1 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
2 bnj953.2 
 |-  ( ( G ` i ) = ( f ` i ) -> A. y ( G ` i ) = ( f ` i ) )
3 bnj312 
 |-  ( ( ( G ` i ) = ( f ` i ) /\ ( G ` suc i ) = ( f ` suc i ) /\ ( i e. _om /\ suc i e. n ) /\ ps ) <-> ( ( G ` suc i ) = ( f ` suc i ) /\ ( G ` i ) = ( f ` i ) /\ ( i e. _om /\ suc i e. n ) /\ ps ) )
4 bnj251 
 |-  ( ( ( G ` suc i ) = ( f ` suc i ) /\ ( G ` i ) = ( f ` i ) /\ ( i e. _om /\ suc i e. n ) /\ ps ) <-> ( ( G ` suc i ) = ( f ` suc i ) /\ ( ( G ` i ) = ( f ` i ) /\ ( ( i e. _om /\ suc i e. n ) /\ ps ) ) ) )
5 3 4 bitri 
 |-  ( ( ( G ` i ) = ( f ` i ) /\ ( G ` suc i ) = ( f ` suc i ) /\ ( i e. _om /\ suc i e. n ) /\ ps ) <-> ( ( G ` suc i ) = ( f ` suc i ) /\ ( ( G ` i ) = ( f ` i ) /\ ( ( i e. _om /\ suc i e. n ) /\ ps ) ) ) )
6 1 bnj115 
 |-  ( ps <-> A. i ( ( i e. _om /\ suc i e. n ) -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
7 sp 
 |-  ( A. i ( ( i e. _om /\ suc i e. n ) -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) -> ( ( i e. _om /\ suc i e. n ) -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
8 7 impcom 
 |-  ( ( ( i e. _om /\ suc i e. n ) /\ A. i ( ( i e. _om /\ suc i e. n ) -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) )
9 6 8 sylan2b 
 |-  ( ( ( i e. _om /\ suc i e. n ) /\ ps ) -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) )
10 2 bnj956 
 |-  ( ( G ` i ) = ( f ` i ) -> U_ y e. ( G ` i ) _pred ( y , A , R ) = U_ y e. ( f ` i ) _pred ( y , A , R ) )
11 eqtr3 
 |-  ( ( ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) /\ U_ y e. ( G ` i ) _pred ( y , A , R ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) -> ( f ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) )
12 9 10 11 syl2anr 
 |-  ( ( ( G ` i ) = ( f ` i ) /\ ( ( i e. _om /\ suc i e. n ) /\ ps ) ) -> ( f ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) )
13 eqtr 
 |-  ( ( ( G ` suc i ) = ( f ` suc i ) /\ ( f ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) )
14 12 13 sylan2 
 |-  ( ( ( G ` suc i ) = ( f ` suc i ) /\ ( ( G ` i ) = ( f ` i ) /\ ( ( i e. _om /\ suc i e. n ) /\ ps ) ) ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) )
15 5 14 sylbi 
 |-  ( ( ( G ` i ) = ( f ` i ) /\ ( G ` suc i ) = ( f ` suc i ) /\ ( i e. _om /\ suc i e. n ) /\ ps ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) )