Step |
Hyp |
Ref |
Expression |
1 |
|
bnj590.1 |
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) |
2 |
|
rsp |
|- ( A. 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 ) ) ) ) |
3 |
1 2
|
sylbi |
|- ( ps -> ( i e. _om -> ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) |
4 |
|
eleq1 |
|- ( B = suc i -> ( B e. n <-> suc i e. n ) ) |
5 |
|
fveqeq2 |
|- ( B = suc i -> ( ( f ` B ) = U_ y e. ( f ` i ) _pred ( y , A , R ) <-> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) |
6 |
4 5
|
imbi12d |
|- ( B = suc i -> ( ( B e. n -> ( f ` B ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) |
7 |
6
|
imbi2d |
|- ( B = suc i -> ( ( i e. _om -> ( B e. n -> ( f ` B ) = 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 |
3 7
|
syl5ibr |
|- ( B = suc i -> ( ps -> ( i e. _om -> ( B e. n -> ( f ` B ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) ) |
9 |
8
|
imp |
|- ( ( B = suc i /\ ps ) -> ( i e. _om -> ( B e. n -> ( f ` B ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) |