Metamath Proof Explorer

Theorem bnj540

Description: Technical lemma for bnj852 . 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 bnj540.1 
|- ( ps <-> A. i e. _om ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj540.2 
|- ( ps" <-> [. G / f ]. ps )
bnj540.3 
|- G e. _V
Assertion bnj540 
|- ( ps" <-> A. i e. _om ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) )

Proof

Step Hyp Ref Expression
1 bnj540.1 
 |-  ( ps <-> A. i e. _om ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
2 bnj540.2 
 |-  ( ps" <-> [. G / f ]. ps )
3 bnj540.3 
 |-  G e. _V
4 1 sbcbii 
 |-  ( [. G / f ]. ps <-> [. G / f ]. A. i e. _om ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
5 3 bnj538 
 |-  ( [. G / f ]. A. i e. _om ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> A. i e. _om [. G / f ]. ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
6 sbcimg 
 |-  ( G e. _V -> ( [. G / f ]. ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> ( [. G / f ]. suc i e. N -> [. G / f ]. ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) )
7 3 6 ax-mp 
 |-  ( [. G / f ]. ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> ( [. G / f ]. suc i e. N -> [. G / f ]. ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
8 7 ralbii 
 |-  ( A. i e. _om [. G / f ]. ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> A. i e. _om ( [. G / f ]. suc i e. N -> [. G / f ]. ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
9 4 5 8 3bitri 
 |-  ( [. G / f ]. ps <-> A. i e. _om ( [. G / f ]. suc i e. N -> [. G / f ]. ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
10 3 bnj525 
 |-  ( [. G / f ]. suc i e. N <-> suc i e. N )
11 fveq1 
 |-  ( f = G -> ( f ` suc i ) = ( G ` suc i ) )
12 fveq1 
 |-  ( f = G -> ( f ` i ) = ( G ` i ) )
13 12 bnj1113 
 |-  ( f = G -> U_ y e. ( f ` i ) _pred ( y , A , R ) = U_ y e. ( G ` i ) _pred ( y , A , R ) )
14 11 13 eqeq12d 
 |-  ( f = G -> ( ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) <-> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) )
15 3 14 sbcie 
 |-  ( [. G / f ]. ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) <-> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) )
16 10 15 imbi12i 
 |-  ( ( [. G / f ]. suc i e. N -> [. G / f ]. ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) )
17 16 ralbii 
 |-  ( A. i e. _om ( [. G / f ]. suc i e. N -> [. G / f ]. ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> A. i e. _om ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) )
18 2 9 17 3bitri 
 |-  ( ps" <-> A. i e. _om ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) )