| Step |
Hyp |
Ref |
Expression |
| 1 |
|
diag1f1.l |
|- L = ( C DiagFunc D ) |
| 2 |
|
diag1f1.c |
|- ( ph -> C e. Cat ) |
| 3 |
|
diag1f1.d |
|- ( ph -> D e. Cat ) |
| 4 |
|
diag1f1.a |
|- A = ( Base ` C ) |
| 5 |
|
diag1f1.b |
|- B = ( Base ` D ) |
| 6 |
|
diag1f1.0 |
|- ( ph -> B =/= (/) ) |
| 7 |
|
eqid |
|- ( D FuncCat C ) = ( D FuncCat C ) |
| 8 |
7
|
fucbas |
|- ( D Func C ) = ( Base ` ( D FuncCat C ) ) |
| 9 |
1 2 3 7
|
diagcl |
|- ( ph -> L e. ( C Func ( D FuncCat C ) ) ) |
| 10 |
9
|
func1st2nd |
|- ( ph -> ( 1st ` L ) ( C Func ( D FuncCat C ) ) ( 2nd ` L ) ) |
| 11 |
4 8 10
|
funcf1 |
|- ( ph -> ( 1st ` L ) : A --> ( D Func C ) ) |
| 12 |
2
|
adantr |
|- ( ( ph /\ ( x e. A /\ y e. A ) ) -> C e. Cat ) |
| 13 |
3
|
adantr |
|- ( ( ph /\ ( x e. A /\ y e. A ) ) -> D e. Cat ) |
| 14 |
6
|
adantr |
|- ( ( ph /\ ( x e. A /\ y e. A ) ) -> B =/= (/) ) |
| 15 |
|
simprl |
|- ( ( ph /\ ( x e. A /\ y e. A ) ) -> x e. A ) |
| 16 |
|
simprr |
|- ( ( ph /\ ( x e. A /\ y e. A ) ) -> y e. A ) |
| 17 |
|
eqid |
|- ( ( 1st ` L ) ` x ) = ( ( 1st ` L ) ` x ) |
| 18 |
|
eqid |
|- ( ( 1st ` L ) ` y ) = ( ( 1st ` L ) ` y ) |
| 19 |
1 12 13 4 5 14 15 16 17 18
|
diag1f1lem |
|- ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( ( ( 1st ` L ) ` x ) = ( ( 1st ` L ) ` y ) -> x = y ) ) |
| 20 |
19
|
ralrimivva |
|- ( ph -> A. x e. A A. y e. A ( ( ( 1st ` L ) ` x ) = ( ( 1st ` L ) ` y ) -> x = y ) ) |
| 21 |
|
dff13 |
|- ( ( 1st ` L ) : A -1-1-> ( D Func C ) <-> ( ( 1st ` L ) : A --> ( D Func C ) /\ A. x e. A A. y e. A ( ( ( 1st ` L ) ` x ) = ( ( 1st ` L ) ` y ) -> x = y ) ) ) |
| 22 |
11 20 21
|
sylanbrc |
|- ( ph -> ( 1st ` L ) : A -1-1-> ( D Func C ) ) |