Metamath Proof Explorer

Theorem prcofpropd

Description: If the categories have the same set of objects, morphisms, and compositions, then they have the same pre-composition functors. (Contributed by Zhi Wang, 21-Nov-2025)

Ref Expression
Hypotheses prcofpropd.1 
|- ( ph -> ( Homf ` A ) = ( Homf ` B ) )
prcofpropd.2 
|- ( ph -> ( comf ` A ) = ( comf ` B ) )
prcofpropd.3 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
prcofpropd.4 
|- ( ph -> ( comf ` C ) = ( comf ` D ) )
prcofpropd.a 
|- ( ph -> A e. V )
prcofpropd.b 
|- ( ph -> B e. V )
prcofpropd.c 
|- ( ph -> C e. V )
prcofpropd.d 
|- ( ph -> D e. V )
prcofpropd.f 
|- ( ph -> F e. W )
Assertion prcofpropd 
|- ( ph -> ( <. A , C >. -o.F F ) = ( <. B , D >. -o.F F ) )

Proof

Step Hyp Ref Expression
1 prcofpropd.1 
 |-  ( ph -> ( Homf ` A ) = ( Homf ` B ) )
2 prcofpropd.2 
 |-  ( ph -> ( comf ` A ) = ( comf ` B ) )
3 prcofpropd.3 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
4 prcofpropd.4 
 |-  ( ph -> ( comf ` C ) = ( comf ` D ) )
5 prcofpropd.a 
 |-  ( ph -> A e. V )
6 prcofpropd.b 
 |-  ( ph -> B e. V )
7 prcofpropd.c 
 |-  ( ph -> C e. V )
8 prcofpropd.d 
 |-  ( ph -> D e. V )
9 prcofpropd.f 
 |-  ( ph -> F e. W )
10 1 2 3 4 5 6 7 8 funcpropd 
 |-  ( ph -> ( A Func C ) = ( B Func D ) )
11 10 mpteq1d 
 |-  ( ph -> ( k e. ( A Func C ) |-> ( k o.func F ) ) = ( k e. ( B Func D ) |-> ( k o.func F ) ) )
12 10 adantr 
 |-  ( ( ph /\ k e. ( A Func C ) ) -> ( A Func C ) = ( B Func D ) )
13 1 adantr 
 |-  ( ( ph /\ ( k e. ( A Func C ) /\ l e. ( A Func C ) ) ) -> ( Homf ` A ) = ( Homf ` B ) )
14 2 adantr 
 |-  ( ( ph /\ ( k e. ( A Func C ) /\ l e. ( A Func C ) ) ) -> ( comf ` A ) = ( comf ` B ) )
15 3 adantr 
 |-  ( ( ph /\ ( k e. ( A Func C ) /\ l e. ( A Func C ) ) ) -> ( Homf ` C ) = ( Homf ` D ) )
16 4 adantr 
 |-  ( ( ph /\ ( k e. ( A Func C ) /\ l e. ( A Func C ) ) ) -> ( comf ` C ) = ( comf ` D ) )
17 funcrcl 
 |-  ( k e. ( A Func C ) -> ( A e. Cat /\ C e. Cat ) )
18 17 ad2antrl 
 |-  ( ( ph /\ ( k e. ( A Func C ) /\ l e. ( A Func C ) ) ) -> ( A e. Cat /\ C e. Cat ) )
19 18 simpld 
 |-  ( ( ph /\ ( k e. ( A Func C ) /\ l e. ( A Func C ) ) ) -> A e. Cat )
20 6 adantr 
 |-  ( ( ph /\ ( k e. ( A Func C ) /\ l e. ( A Func C ) ) ) -> B e. V )
21 13 14 19 20 catpropd 
 |-  ( ( ph /\ ( k e. ( A Func C ) /\ l e. ( A Func C ) ) ) -> ( A e. Cat <-> B e. Cat ) )
22 19 21 mpbid 
 |-  ( ( ph /\ ( k e. ( A Func C ) /\ l e. ( A Func C ) ) ) -> B e. Cat )
23 18 simprd 
 |-  ( ( ph /\ ( k e. ( A Func C ) /\ l e. ( A Func C ) ) ) -> C e. Cat )
24 8 adantr 
 |-  ( ( ph /\ ( k e. ( A Func C ) /\ l e. ( A Func C ) ) ) -> D e. V )
25 15 16 23 24 catpropd 
 |-  ( ( ph /\ ( k e. ( A Func C ) /\ l e. ( A Func C ) ) ) -> ( C e. Cat <-> D e. Cat ) )
26 23 25 mpbid 
 |-  ( ( ph /\ ( k e. ( A Func C ) /\ l e. ( A Func C ) ) ) -> D e. Cat )
27 13 14 15 16 19 22 23 26 natpropd 
 |-  ( ( ph /\ ( k e. ( A Func C ) /\ l e. ( A Func C ) ) ) -> ( A Nat C ) = ( B Nat D ) )
28 27 oveqd 
 |-  ( ( ph /\ ( k e. ( A Func C ) /\ l e. ( A Func C ) ) ) -> ( k ( A Nat C ) l ) = ( k ( B Nat D ) l ) )
29 28 mpteq1d 
 |-  ( ( ph /\ ( k e. ( A Func C ) /\ l e. ( A Func C ) ) ) -> ( a e. ( k ( A Nat C ) l ) |-> ( a o. ( 1st ` F ) ) ) = ( a e. ( k ( B Nat D ) l ) |-> ( a o. ( 1st ` F ) ) ) )
30 10 12 29 mpoeq123dva 
 |-  ( ph -> ( k e. ( A Func C ) , l e. ( A Func C ) |-> ( a e. ( k ( A Nat C ) l ) |-> ( a o. ( 1st ` F ) ) ) ) = ( k e. ( B Func D ) , l e. ( B Func D ) |-> ( a e. ( k ( B Nat D ) l ) |-> ( a o. ( 1st ` F ) ) ) ) )
31 11 30 opeq12d 
 |-  ( ph -> <. ( k e. ( A Func C ) |-> ( k o.func F ) ) , ( k e. ( A Func C ) , l e. ( A Func C ) |-> ( a e. ( k ( A Nat C ) l ) |-> ( a o. ( 1st ` F ) ) ) ) >. = <. ( k e. ( B Func D ) |-> ( k o.func F ) ) , ( k e. ( B Func D ) , l e. ( B Func D ) |-> ( a e. ( k ( B Nat D ) l ) |-> ( a o. ( 1st ` F ) ) ) ) >. )
32 eqid 
 |-  ( A Func C ) = ( A Func C )
33 eqid 
 |-  ( A Nat C ) = ( A Nat C )
34 32 33 5 7 9 prcofvala 
 |-  ( ph -> ( <. A , C >. -o.F F ) = <. ( k e. ( A Func C ) |-> ( k o.func F ) ) , ( k e. ( A Func C ) , l e. ( A Func C ) |-> ( a e. ( k ( A Nat C ) l ) |-> ( a o. ( 1st ` F ) ) ) ) >. )
35 eqid 
 |-  ( B Func D ) = ( B Func D )
36 eqid 
 |-  ( B Nat D ) = ( B Nat D )
37 35 36 6 8 9 prcofvala 
 |-  ( ph -> ( <. B , D >. -o.F F ) = <. ( k e. ( B Func D ) |-> ( k o.func F ) ) , ( k e. ( B Func D ) , l e. ( B Func D ) |-> ( a e. ( k ( B Nat D ) l ) |-> ( a o. ( 1st ` F ) ) ) ) >. )
38 31 34 37 3eqtr4d 
 |-  ( ph -> ( <. A , C >. -o.F F ) = ( <. B , D >. -o.F F ) )