Metamath Proof Explorer

Theorem fuco11bALT

Description: Alternate proof of fuco11b . (Contributed by Zhi Wang, 11-Oct-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses fuco11b.o 
|- ( ph -> ( 1st ` ( <. C , D >. o.F E ) ) = O )
fuco11b.f 
|- ( ph -> F e. ( C Func D ) )
fuco11b.g 
|- ( ph -> G e. ( D Func E ) )
Assertion fuco11bALT 
|- ( ph -> ( G O F ) = ( G o.func F ) )

Proof

Step Hyp Ref Expression
1 fuco11b.o 
 |-  ( ph -> ( 1st ` ( <. C , D >. o.F E ) ) = O )
2 fuco11b.f 
 |-  ( ph -> F e. ( C Func D ) )
3 fuco11b.g 
 |-  ( ph -> G e. ( D Func E ) )
4 df-ov 
 |-  ( G O F ) = ( O ` <. G , F >. )
5 relfunc 
 |-  Rel ( D Func E )
6 1st2nd 
 |-  ( ( Rel ( D Func E ) /\ G e. ( D Func E ) ) -> G = <. ( 1st ` G ) , ( 2nd ` G ) >. )
7 5 3 6 sylancr 
 |-  ( ph -> G = <. ( 1st ` G ) , ( 2nd ` G ) >. )
8 relfunc 
 |-  Rel ( C Func D )
9 1st2nd 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
10 8 2 9 sylancr 
 |-  ( ph -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
11 7 10 oveq12d 
 |-  ( ph -> ( G o.func F ) = ( <. ( 1st ` G ) , ( 2nd ` G ) >. o.func <. ( 1st ` F ) , ( 2nd ` F ) >. ) )
12 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
13 8 2 12 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
14 13 funcrcl2 
 |-  ( ph -> C e. Cat )
15 1st2ndbr 
 |-  ( ( Rel ( D Func E ) /\ G e. ( D Func E ) ) -> ( 1st ` G ) ( D Func E ) ( 2nd ` G ) )
16 5 3 15 sylancr 
 |-  ( ph -> ( 1st ` G ) ( D Func E ) ( 2nd ` G ) )
17 16 funcrcl2 
 |-  ( ph -> D e. Cat )
18 16 funcrcl3 
 |-  ( ph -> E e. Cat )
19 eqidd 
 |-  ( ph -> ( <. C , D >. o.F E ) = ( <. C , D >. o.F E ) )
20 14 17 18 19 fucoelvv 
 |-  ( ph -> ( <. C , D >. o.F E ) e. ( _V X. _V ) )
21 1st2nd2 
 |-  ( ( <. C , D >. o.F E ) e. ( _V X. _V ) -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. )
22 20 21 syl 
 |-  ( ph -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. )
23 7 10 opeq12d 
 |-  ( ph -> <. G , F >. = <. <. ( 1st ` G ) , ( 2nd ` G ) >. , <. ( 1st ` F ) , ( 2nd ` F ) >. >. )
24 22 13 16 23 fuco11 
 |-  ( ph -> ( ( 1st ` ( <. C , D >. o.F E ) ) ` <. G , F >. ) = ( <. ( 1st ` G ) , ( 2nd ` G ) >. o.func <. ( 1st ` F ) , ( 2nd ` F ) >. ) )
25 1 fveq1d 
 |-  ( ph -> ( ( 1st ` ( <. C , D >. o.F E ) ) ` <. G , F >. ) = ( O ` <. G , F >. ) )
26 11 24 25 3eqtr2rd 
 |-  ( ph -> ( O ` <. G , F >. ) = ( G o.func F ) )
27 4 26 eqtrid 
 |-  ( ph -> ( G O F ) = ( G o.func F ) )