Metamath Proof Explorer

Theorem dfinito3

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

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

Proof

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