| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cofu1a.b |
|- B = ( Base ` C ) |
| 2 |
|
cofu1a.f |
|- ( ph -> F ( C Func D ) G ) |
| 3 |
|
cofu1a.k |
|- ( ph -> K ( D Func E ) L ) |
| 4 |
|
cofu1a.m |
|- ( ph -> ( <. K , L >. o.func <. F , G >. ) = <. M , N >. ) |
| 5 |
|
cofu1a.x |
|- ( ph -> X e. B ) |
| 6 |
|
df-br |
|- ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) ) |
| 7 |
2 6
|
sylib |
|- ( ph -> <. F , G >. e. ( C Func D ) ) |
| 8 |
|
df-br |
|- ( K ( D Func E ) L <-> <. K , L >. e. ( D Func E ) ) |
| 9 |
3 8
|
sylib |
|- ( ph -> <. K , L >. e. ( D Func E ) ) |
| 10 |
1 7 9 5
|
cofu1 |
|- ( ph -> ( ( 1st ` ( <. K , L >. o.func <. F , G >. ) ) ` X ) = ( ( 1st ` <. K , L >. ) ` ( ( 1st ` <. F , G >. ) ` X ) ) ) |
| 11 |
4
|
fveq2d |
|- ( ph -> ( 1st ` ( <. K , L >. o.func <. F , G >. ) ) = ( 1st ` <. M , N >. ) ) |
| 12 |
7 9
|
cofucl |
|- ( ph -> ( <. K , L >. o.func <. F , G >. ) e. ( C Func E ) ) |
| 13 |
4 12
|
eqeltrrd |
|- ( ph -> <. M , N >. e. ( C Func E ) ) |
| 14 |
|
df-br |
|- ( M ( C Func E ) N <-> <. M , N >. e. ( C Func E ) ) |
| 15 |
13 14
|
sylibr |
|- ( ph -> M ( C Func E ) N ) |
| 16 |
15
|
func1st |
|- ( ph -> ( 1st ` <. M , N >. ) = M ) |
| 17 |
11 16
|
eqtrd |
|- ( ph -> ( 1st ` ( <. K , L >. o.func <. F , G >. ) ) = M ) |
| 18 |
17
|
fveq1d |
|- ( ph -> ( ( 1st ` ( <. K , L >. o.func <. F , G >. ) ) ` X ) = ( M ` X ) ) |
| 19 |
3
|
func1st |
|- ( ph -> ( 1st ` <. K , L >. ) = K ) |
| 20 |
2
|
func1st |
|- ( ph -> ( 1st ` <. F , G >. ) = F ) |
| 21 |
20
|
fveq1d |
|- ( ph -> ( ( 1st ` <. F , G >. ) ` X ) = ( F ` X ) ) |
| 22 |
19 21
|
fveq12d |
|- ( ph -> ( ( 1st ` <. K , L >. ) ` ( ( 1st ` <. F , G >. ) ` X ) ) = ( K ` ( F ` X ) ) ) |
| 23 |
10 18 22
|
3eqtr3rd |
|- ( ph -> ( K ` ( F ` X ) ) = ( M ` X ) ) |