Metamath Proof Explorer

Theorem bnj539

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 bnj539.1 
|- ( ps <-> A. i e. _om ( suc i e. n -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) )
bnj539.2 
|- ( ps' <-> [. M / n ]. ps )
bnj539.3 
|- M e. _V
Assertion bnj539 
|- ( ps' <-> A. i e. _om ( suc i e. M -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) )

Proof

Step Hyp Ref Expression
1 bnj539.1 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) )
2 bnj539.2 
 |-  ( ps' <-> [. M / n ]. ps )
3 bnj539.3 
 |-  M e. _V
4 1 sbcbii 
 |-  ( [. M / n ]. ps <-> [. M / n ]. A. i e. _om ( suc i e. n -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) )
5 3 bnj538 
 |-  ( [. M / n ]. A. i e. _om ( suc i e. n -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) <-> A. i e. _om [. M / n ]. ( suc i e. n -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) )
6 sbcimg 
 |-  ( M e. _V -> ( [. M / n ]. ( suc i e. n -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) <-> ( [. M / n ]. suc i e. n -> [. M / n ]. ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) ) )
7 3 6 ax-mp 
 |-  ( [. M / n ]. ( suc i e. n -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) <-> ( [. M / n ]. suc i e. n -> [. M / n ]. ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) )
8 sbcel2gv 
 |-  ( M e. _V -> ( [. M / n ]. suc i e. n <-> suc i e. M ) )
9 3 8 ax-mp 
 |-  ( [. M / n ]. suc i e. n <-> suc i e. M )
10 3 bnj525 
 |-  ( [. M / 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 ) )
11 9 10 imbi12i 
 |-  ( ( [. M / n ]. suc i e. n -> [. M / n ]. ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) <-> ( suc i e. M -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) )
12 7 11 bitri 
 |-  ( [. M / n ]. ( suc i e. n -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) <-> ( suc i e. M -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) )
13 12 ralbii 
 |-  ( A. i e. _om [. M / n ]. ( suc i e. n -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) <-> A. i e. _om ( suc i e. M -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) )
14 5 13 bitri 
 |-  ( [. M / n ]. A. i e. _om ( suc i e. n -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) <-> A. i e. _om ( suc i e. M -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) )
15 4 14 bitri 
 |-  ( [. M / n ]. ps <-> A. i e. _om ( suc i e. M -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) )
16 2 15 bitri 
 |-  ( ps' <-> A. i e. _om ( suc i e. M -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) )