Step |
Hyp |
Ref |
Expression |
1 |
|
0ssc |
|- ( C e. Cat -> (/) C_cat ( Homf ` C ) ) |
2 |
|
ral0 |
|- A. x e. (/) ( ( ( Id ` C ) ` x ) e. ( x (/) x ) /\ A. y e. (/) A. z e. (/) A. f e. ( x (/) y ) A. g e. ( y (/) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x (/) z ) ) |
3 |
2
|
a1i |
|- ( C e. Cat -> A. x e. (/) ( ( ( Id ` C ) ` x ) e. ( x (/) x ) /\ A. y e. (/) A. z e. (/) A. f e. ( x (/) y ) A. g e. ( y (/) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x (/) z ) ) ) |
4 |
|
eqid |
|- ( Homf ` C ) = ( Homf ` C ) |
5 |
|
eqid |
|- ( Id ` C ) = ( Id ` C ) |
6 |
|
eqid |
|- ( comp ` C ) = ( comp ` C ) |
7 |
|
id |
|- ( C e. Cat -> C e. Cat ) |
8 |
|
f0 |
|- (/) : (/) --> (/) |
9 |
|
ffn |
|- ( (/) : (/) --> (/) -> (/) Fn (/) ) |
10 |
8 9
|
ax-mp |
|- (/) Fn (/) |
11 |
|
0xp |
|- ( (/) X. (/) ) = (/) |
12 |
11
|
fneq2i |
|- ( (/) Fn ( (/) X. (/) ) <-> (/) Fn (/) ) |
13 |
10 12
|
mpbir |
|- (/) Fn ( (/) X. (/) ) |
14 |
13
|
a1i |
|- ( C e. Cat -> (/) Fn ( (/) X. (/) ) ) |
15 |
4 5 6 7 14
|
issubc2 |
|- ( C e. Cat -> ( (/) e. ( Subcat ` C ) <-> ( (/) C_cat ( Homf ` C ) /\ A. x e. (/) ( ( ( Id ` C ) ` x ) e. ( x (/) x ) /\ A. y e. (/) A. z e. (/) A. f e. ( x (/) y ) A. g e. ( y (/) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x (/) z ) ) ) ) ) |
16 |
1 3 15
|
mpbir2and |
|- ( C e. Cat -> (/) e. ( Subcat ` C ) ) |