Step |
Hyp |
Ref |
Expression |
1 |
|
bnj106.1 |
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) |
2 |
|
bnj106.2 |
|- F e. _V |
3 |
|
bnj105 |
|- 1o e. _V |
4 |
1 3
|
bnj92 |
|- ( [. 1o / n ]. ps <-> A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) |
5 |
4
|
sbcbii |
|- ( [. F / f ]. [. 1o / n ]. ps <-> [. F / f ]. A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) |
6 |
|
fveq1 |
|- ( f = F -> ( f ` suc i ) = ( F ` suc i ) ) |
7 |
|
fveq1 |
|- ( f = F -> ( f ` i ) = ( F ` i ) ) |
8 |
7
|
bnj1113 |
|- ( f = F -> U_ y e. ( f ` i ) _pred ( y , A , R ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) |
9 |
6 8
|
eqeq12d |
|- ( f = F -> ( ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) <-> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) ) |
10 |
9
|
imbi2d |
|- ( f = F -> ( ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) ) ) |
11 |
10
|
ralbidv |
|- ( f = F -> ( A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> A. i e. _om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) ) ) |
12 |
2 11
|
sbcie |
|- ( [. F / f ]. A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> A. i e. _om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) ) |
13 |
5 12
|
bitri |
|- ( [. 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 ) ) ) |