Step |
Hyp |
Ref |
Expression |
1 |
|
isinito.b |
|- B = ( Base ` C ) |
2 |
|
isinito.h |
|- H = ( Hom ` C ) |
3 |
|
isinito.c |
|- ( ph -> C e. Cat ) |
4 |
|
isinito.i |
|- ( ph -> I e. B ) |
5 |
3 1 2
|
termoval |
|- ( ph -> ( TermO ` C ) = { i e. B | A. b e. B E! h h e. ( b H i ) } ) |
6 |
5
|
eleq2d |
|- ( ph -> ( I e. ( TermO ` C ) <-> I e. { i e. B | A. b e. B E! h h e. ( b H i ) } ) ) |
7 |
|
oveq2 |
|- ( i = I -> ( b H i ) = ( b H I ) ) |
8 |
7
|
eleq2d |
|- ( i = I -> ( h e. ( b H i ) <-> h e. ( b H I ) ) ) |
9 |
8
|
eubidv |
|- ( i = I -> ( E! h h e. ( b H i ) <-> E! h h e. ( b H I ) ) ) |
10 |
9
|
ralbidv |
|- ( i = I -> ( A. b e. B E! h h e. ( b H i ) <-> A. b e. B E! h h e. ( b H I ) ) ) |
11 |
10
|
elrab3 |
|- ( I e. B -> ( I e. { i e. B | A. b e. B E! h h e. ( b H i ) } <-> A. b e. B E! h h e. ( b H I ) ) ) |
12 |
4 11
|
syl |
|- ( ph -> ( I e. { i e. B | A. b e. B E! h h e. ( b H i ) } <-> A. b e. B E! h h e. ( b H I ) ) ) |
13 |
6 12
|
bitrd |
|- ( ph -> ( I e. ( TermO ` C ) <-> A. b e. B E! h h e. ( b H I ) ) ) |