Step |
Hyp |
Ref |
Expression |
1 |
|
isinitoi.b |
|- B = ( Base ` C ) |
2 |
|
isinitoi.h |
|- H = ( Hom ` C ) |
3 |
|
isinitoi.c |
|- ( ph -> C e. Cat ) |
4 |
1 2 3
|
istermoi |
|- ( ( ph /\ O e. ( TermO ` C ) ) -> ( O e. B /\ A. o e. B E! h h e. ( o H O ) ) ) |
5 |
|
oveq1 |
|- ( o = O -> ( o H O ) = ( O H O ) ) |
6 |
5
|
eleq2d |
|- ( o = O -> ( h e. ( o H O ) <-> h e. ( O H O ) ) ) |
7 |
6
|
eubidv |
|- ( o = O -> ( E! h h e. ( o H O ) <-> E! h h e. ( O H O ) ) ) |
8 |
7
|
rspcv |
|- ( O e. B -> ( A. o e. B E! h h e. ( o H O ) -> E! h h e. ( O H O ) ) ) |
9 |
8
|
adantl |
|- ( ( ( ph /\ O e. ( TermO ` C ) ) /\ O e. B ) -> ( A. o e. B E! h h e. ( o H O ) -> E! h h e. ( O H O ) ) ) |
10 |
|
eusn |
|- ( E! h h e. ( O H O ) <-> E. h ( O H O ) = { h } ) |
11 |
|
eqid |
|- ( Id ` C ) = ( Id ` C ) |
12 |
3
|
ad2antrr |
|- ( ( ( ph /\ O e. ( TermO ` C ) ) /\ O e. B ) -> C e. Cat ) |
13 |
|
simpr |
|- ( ( ( ph /\ O e. ( TermO ` C ) ) /\ O e. B ) -> O e. B ) |
14 |
1 2 11 12 13
|
catidcl |
|- ( ( ( ph /\ O e. ( TermO ` C ) ) /\ O e. B ) -> ( ( Id ` C ) ` O ) e. ( O H O ) ) |
15 |
|
fvex |
|- ( ( Id ` C ) ` O ) e. _V |
16 |
15
|
elsn |
|- ( ( ( Id ` C ) ` O ) e. { h } <-> ( ( Id ` C ) ` O ) = h ) |
17 |
|
eqcom |
|- ( ( ( Id ` C ) ` O ) = h <-> h = ( ( Id ` C ) ` O ) ) |
18 |
|
sneqbg |
|- ( h e. _V -> ( { h } = { ( ( Id ` C ) ` O ) } <-> h = ( ( Id ` C ) ` O ) ) ) |
19 |
18
|
bicomd |
|- ( h e. _V -> ( h = ( ( Id ` C ) ` O ) <-> { h } = { ( ( Id ` C ) ` O ) } ) ) |
20 |
19
|
elv |
|- ( h = ( ( Id ` C ) ` O ) <-> { h } = { ( ( Id ` C ) ` O ) } ) |
21 |
16 17 20
|
3bitri |
|- ( ( ( Id ` C ) ` O ) e. { h } <-> { h } = { ( ( Id ` C ) ` O ) } ) |
22 |
21
|
biimpi |
|- ( ( ( Id ` C ) ` O ) e. { h } -> { h } = { ( ( Id ` C ) ` O ) } ) |
23 |
22
|
a1i |
|- ( ( O H O ) = { h } -> ( ( ( Id ` C ) ` O ) e. { h } -> { h } = { ( ( Id ` C ) ` O ) } ) ) |
24 |
|
eleq2 |
|- ( ( O H O ) = { h } -> ( ( ( Id ` C ) ` O ) e. ( O H O ) <-> ( ( Id ` C ) ` O ) e. { h } ) ) |
25 |
|
eqeq1 |
|- ( ( O H O ) = { h } -> ( ( O H O ) = { ( ( Id ` C ) ` O ) } <-> { h } = { ( ( Id ` C ) ` O ) } ) ) |
26 |
23 24 25
|
3imtr4d |
|- ( ( O H O ) = { h } -> ( ( ( Id ` C ) ` O ) e. ( O H O ) -> ( O H O ) = { ( ( Id ` C ) ` O ) } ) ) |
27 |
14 26
|
syl5 |
|- ( ( O H O ) = { h } -> ( ( ( ph /\ O e. ( TermO ` C ) ) /\ O e. B ) -> ( O H O ) = { ( ( Id ` C ) ` O ) } ) ) |
28 |
27
|
exlimiv |
|- ( E. h ( O H O ) = { h } -> ( ( ( ph /\ O e. ( TermO ` C ) ) /\ O e. B ) -> ( O H O ) = { ( ( Id ` C ) ` O ) } ) ) |
29 |
28
|
com12 |
|- ( ( ( ph /\ O e. ( TermO ` C ) ) /\ O e. B ) -> ( E. h ( O H O ) = { h } -> ( O H O ) = { ( ( Id ` C ) ` O ) } ) ) |
30 |
10 29
|
syl5bi |
|- ( ( ( ph /\ O e. ( TermO ` C ) ) /\ O e. B ) -> ( E! h h e. ( O H O ) -> ( O H O ) = { ( ( Id ` C ) ` O ) } ) ) |
31 |
9 30
|
syld |
|- ( ( ( ph /\ O e. ( TermO ` C ) ) /\ O e. B ) -> ( A. o e. B E! h h e. ( o H O ) -> ( O H O ) = { ( ( Id ` C ) ` O ) } ) ) |
32 |
31
|
expimpd |
|- ( ( ph /\ O e. ( TermO ` C ) ) -> ( ( O e. B /\ A. o e. B E! h h e. ( o H O ) ) -> ( O H O ) = { ( ( Id ` C ) ` O ) } ) ) |
33 |
4 32
|
mpd |
|- ( ( ph /\ O e. ( TermO ` C ) ) -> ( O H O ) = { ( ( Id ` C ) ` O ) } ) |