Metamath Proof Explorer

Theorem prcof1

Description: The object part of the pre-composition functor. (Contributed by Zhi Wang, 3-Nov-2025)

Ref Expression
Hypotheses prcof1.k 
|- ( ph -> K e. ( D Func E ) )
prcof1.o 
|- ( ph -> ( 1st ` ( <. D , E >. -o.F F ) ) = O )
Assertion prcof1 
|- ( ph -> ( O ` K ) = ( K o.func F ) )

Proof

Step Hyp Ref Expression
1 prcof1.k 
 |-  ( ph -> K e. ( D Func E ) )
2 prcof1.o 
 |-  ( ph -> ( 1st ` ( <. D , E >. -o.F F ) ) = O )
3 2 adantr 
 |-  ( ( ph /\ F e. _V ) -> ( 1st ` ( <. D , E >. -o.F F ) ) = O )
4 eqid 
 |-  ( D Func E ) = ( D Func E )
5 eqid 
 |-  ( D Nat E ) = ( D Nat E )
6 1 adantr 
 |-  ( ( ph /\ F e. _V ) -> K e. ( D Func E ) )
7 6 func1st2nd 
 |-  ( ( ph /\ F e. _V ) -> ( 1st ` K ) ( D Func E ) ( 2nd ` K ) )
8 7 funcrcl2 
 |-  ( ( ph /\ F e. _V ) -> D e. Cat )
9 7 funcrcl3 
 |-  ( ( ph /\ F e. _V ) -> E e. Cat )
10 simpr 
 |-  ( ( ph /\ F e. _V ) -> F e. _V )
11 4 5 8 9 10 prcofvala 
 |-  ( ( ph /\ F e. _V ) -> ( <. D , E >. -o.F F ) = <. ( k e. ( D Func E ) |-> ( k o.func F ) ) , ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k ( D Nat E ) l ) |-> ( a o. ( 1st ` F ) ) ) ) >. )
12 11 fveq2d 
 |-  ( ( ph /\ F e. _V ) -> ( 1st ` ( <. D , E >. -o.F F ) ) = ( 1st ` <. ( k e. ( D Func E ) |-> ( k o.func F ) ) , ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k ( D Nat E ) l ) |-> ( a o. ( 1st ` F ) ) ) ) >. ) )
13 ovex 
 |-  ( D Func E ) e. _V
14 13 mptex 
 |-  ( k e. ( D Func E ) |-> ( k o.func F ) ) e. _V
15 13 13 mpoex 
 |-  ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k ( D Nat E ) l ) |-> ( a o. ( 1st ` F ) ) ) ) e. _V
16 14 15 op1st 
 |-  ( 1st ` <. ( k e. ( D Func E ) |-> ( k o.func F ) ) , ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k ( D Nat E ) l ) |-> ( a o. ( 1st ` F ) ) ) ) >. ) = ( k e. ( D Func E ) |-> ( k o.func F ) )
17 12 16 eqtrdi 
 |-  ( ( ph /\ F e. _V ) -> ( 1st ` ( <. D , E >. -o.F F ) ) = ( k e. ( D Func E ) |-> ( k o.func F ) ) )
18 3 17 eqtr3d 
 |-  ( ( ph /\ F e. _V ) -> O = ( k e. ( D Func E ) |-> ( k o.func F ) ) )
19 simpr 
 |-  ( ( ( ph /\ F e. _V ) /\ k = K ) -> k = K )
20 19 oveq1d 
 |-  ( ( ( ph /\ F e. _V ) /\ k = K ) -> ( k o.func F ) = ( K o.func F ) )
21 ovexd 
 |-  ( ( ph /\ F e. _V ) -> ( K o.func F ) e. _V )
22 18 20 6 21 fvmptd 
 |-  ( ( ph /\ F e. _V ) -> ( O ` K ) = ( K o.func F ) )
23 0fv 
 |-  ( (/) ` K ) = (/)
24 reldmprcof 
 |-  Rel dom -o.F
25 24 ovprc2 
 |-  ( -. F e. _V -> ( <. D , E >. -o.F F ) = (/) )
26 25 fveq2d 
 |-  ( -. F e. _V -> ( 1st ` ( <. D , E >. -o.F F ) ) = ( 1st ` (/) ) )
27 1st0 
 |-  ( 1st ` (/) ) = (/)
28 26 27 eqtrdi 
 |-  ( -. F e. _V -> ( 1st ` ( <. D , E >. -o.F F ) ) = (/) )
29 2 28 sylan9req 
 |-  ( ( ph /\ -. F e. _V ) -> O = (/) )
30 29 fveq1d 
 |-  ( ( ph /\ -. F e. _V ) -> ( O ` K ) = ( (/) ` K ) )
31 df-cofu 
 |-  o.func = ( l e. _V , k e. _V |-> <. ( ( 1st ` l ) o. ( 1st ` k ) ) , ( a e. dom dom ( 2nd ` k ) , b e. dom dom ( 2nd ` k ) |-> ( ( ( ( 1st ` k ) ` a ) ( 2nd ` l ) ( ( 1st ` k ) ` b ) ) o. ( a ( 2nd ` k ) b ) ) ) >. )
32 31 reldmmpo 
 |-  Rel dom o.func
33 32 ovprc2 
 |-  ( -. F e. _V -> ( K o.func F ) = (/) )
34 33 adantl 
 |-  ( ( ph /\ -. F e. _V ) -> ( K o.func F ) = (/) )
35 23 30 34 3eqtr4a 
 |-  ( ( ph /\ -. F e. _V ) -> ( O ` K ) = ( K o.func F ) )
36 22 35 pm2.61dan 
 |-  ( ph -> ( O ` K ) = ( K o.func F ) )