Metamath Proof Explorer

Theorem dftermo3

Description: An alternate definition of df-termo depending on df-inito , without dummy variables. (Contributed by Zhi Wang, 29-Aug-2024)

Ref Expression
Assertion dftermo3 
|- TermO = ( InitO o. ( oppCat |` Cat ) )

Proof

Step Hyp Ref Expression
1 fvres 
 |-  ( c e. Cat -> ( ( oppCat |` Cat ) ` c ) = ( oppCat ` c ) )
2 1 fveq2d 
 |-  ( c e. Cat -> ( InitO ` ( ( oppCat |` Cat ) ` c ) ) = ( InitO ` ( oppCat ` c ) ) )
3 2 mpteq2ia 
 |-  ( c e. Cat |-> ( InitO ` ( ( oppCat |` Cat ) ` c ) ) ) = ( c e. Cat |-> ( InitO ` ( oppCat ` c ) ) )
4 initofn 
 |-  InitO Fn Cat
5 dffn2 
 |-  ( InitO Fn Cat <-> InitO : Cat --> _V )
6 4 5 mpbi 
 |-  InitO : Cat --> _V
7 oppccatf 
 |-  ( oppCat |` Cat ) : Cat --> Cat
8 fcompt 
 |-  ( ( InitO : Cat --> _V /\ ( oppCat |` Cat ) : Cat --> Cat ) -> ( InitO o. ( oppCat |` Cat ) ) = ( c e. Cat |-> ( InitO ` ( ( oppCat |` Cat ) ` c ) ) ) )
9 6 7 8 mp2an 
 |-  ( InitO o. ( oppCat |` Cat ) ) = ( c e. Cat |-> ( InitO ` ( ( oppCat |` Cat ) ` c ) ) )
10 dftermo2 
 |-  TermO = ( c e. Cat |-> ( InitO ` ( oppCat ` c ) ) )
11 3 9 10 3eqtr4ri 
 |-  TermO = ( InitO o. ( oppCat |` Cat ) )