Metamath Proof Explorer


Theorem bnj126

Description: Technical lemma for bnj150 . 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 bnj126.1
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj126.2
|- ( ps' <-> [. 1o / n ]. ps )
bnj126.3
|- ( ps" <-> [. F / f ]. ps' )
bnj126.4
|- F = { <. (/) , _pred ( x , A , R ) >. }
Assertion bnj126
|- ( ps" <-> A. i e. _om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) )

Proof

Step Hyp Ref Expression
1 bnj126.1
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
2 bnj126.2
 |-  ( ps' <-> [. 1o / n ]. ps )
3 bnj126.3
 |-  ( ps" <-> [. F / f ]. ps' )
4 bnj126.4
 |-  F = { <. (/) , _pred ( x , A , R ) >. }
5 2 sbcbii
 |-  ( [. F / f ]. ps' <-> [. F / f ]. [. 1o / n ]. ps )
6 4 bnj95
 |-  F e. _V
7 1 6 bnj106
 |-  ( [. F / f ]. [. 1o / n ]. ps <-> A. i e. _om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) )
8 3 5 7 3bitri
 |-  ( ps" <-> A. i e. _om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) )