Step |
Hyp |
Ref |
Expression |
1 |
|
bnj222.1 |
|- ( ps <-> A. i e. _om ( suc i e. N -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) ) |
2 |
|
suceq |
|- ( i = m -> suc i = suc m ) |
3 |
2
|
eleq1d |
|- ( i = m -> ( suc i e. N <-> suc m e. N ) ) |
4 |
2
|
fveq2d |
|- ( i = m -> ( F ` suc i ) = ( F ` suc m ) ) |
5 |
|
fveq2 |
|- ( i = m -> ( F ` i ) = ( F ` m ) ) |
6 |
5
|
bnj1113 |
|- ( i = m -> U_ y e. ( F ` i ) _pred ( y , A , R ) = U_ y e. ( F ` m ) _pred ( y , A , R ) ) |
7 |
4 6
|
eqeq12d |
|- ( i = m -> ( ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) <-> ( F ` suc m ) = U_ y e. ( F ` m ) _pred ( y , A , R ) ) ) |
8 |
3 7
|
imbi12d |
|- ( i = m -> ( ( suc i e. N -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) <-> ( suc m e. N -> ( F ` suc m ) = U_ y e. ( F ` m ) _pred ( y , A , R ) ) ) ) |
9 |
8
|
cbvralvw |
|- ( A. i e. _om ( suc i e. N -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) <-> A. m e. _om ( suc m e. N -> ( F ` suc m ) = U_ y e. ( F ` m ) _pred ( y , A , R ) ) ) |
10 |
1 9
|
bitri |
|- ( ps <-> A. m e. _om ( suc m e. N -> ( F ` suc m ) = U_ y e. ( F ` m ) _pred ( y , A , R ) ) ) |