Metamath Proof Explorer

Theorem prcofelvv

Description: The pre-composition functor is an ordered pair. (Contributed by Zhi Wang, 4-Nov-2025)

Ref Expression
Hypotheses prcofelvv.f 
|- ( ph -> F e. U )
prcofelvv.p 
|- ( ph -> P e. V )
Assertion prcofelvv 
|- ( ph -> ( P -o.F F ) e. ( _V X. _V ) )

Proof

Step Hyp Ref Expression
1 prcofelvv.f 
 |-  ( ph -> F e. U )
2 prcofelvv.p 
 |-  ( ph -> P e. V )
3 eqid 
 |-  ( ( 1st ` P ) Func ( 2nd ` P ) ) = ( ( 1st ` P ) Func ( 2nd ` P ) )
4 eqid 
 |-  ( ( 1st ` P ) Nat ( 2nd ` P ) ) = ( ( 1st ` P ) Nat ( 2nd ` P ) )
5 eqidd 
 |-  ( ph -> ( 1st ` P ) = ( 1st ` P ) )
6 eqidd 
 |-  ( ph -> ( 2nd ` P ) = ( 2nd ` P ) )
7 3 4 1 2 5 6 prcofvalg 
 |-  ( ph -> ( P -o.F F ) = <. ( k e. ( ( 1st ` P ) Func ( 2nd ` P ) ) |-> ( k o.func F ) ) , ( k e. ( ( 1st ` P ) Func ( 2nd ` P ) ) , l e. ( ( 1st ` P ) Func ( 2nd ` P ) ) |-> ( a e. ( k ( ( 1st ` P ) Nat ( 2nd ` P ) ) l ) |-> ( a o. ( 1st ` F ) ) ) ) >. )
8 ovex 
 |-  ( ( 1st ` P ) Func ( 2nd ` P ) ) e. _V
9 8 mptex 
 |-  ( k e. ( ( 1st ` P ) Func ( 2nd ` P ) ) |-> ( k o.func F ) ) e. _V
10 8 8 mpoex 
 |-  ( k e. ( ( 1st ` P ) Func ( 2nd ` P ) ) , l e. ( ( 1st ` P ) Func ( 2nd ` P ) ) |-> ( a e. ( k ( ( 1st ` P ) Nat ( 2nd ` P ) ) l ) |-> ( a o. ( 1st ` F ) ) ) ) e. _V
11 9 10 opelvv 
 |-  <. ( k e. ( ( 1st ` P ) Func ( 2nd ` P ) ) |-> ( k o.func F ) ) , ( k e. ( ( 1st ` P ) Func ( 2nd ` P ) ) , l e. ( ( 1st ` P ) Func ( 2nd ` P ) ) |-> ( a e. ( k ( ( 1st ` P ) Nat ( 2nd ` P ) ) l ) |-> ( a o. ( 1st ` F ) ) ) ) >. e. ( _V X. _V )
12 7 11 eqeltrdi 
 |-  ( ph -> ( P -o.F F ) e. ( _V X. _V ) )