Metamath Proof Explorer

Theorem oppccatf

Description: oppCat restricted to Cat is a function from Cat to Cat . (Contributed by Zhi Wang, 29-Aug-2024)

Ref Expression
Assertion oppccatf 
|- ( oppCat |` Cat ) : Cat --> Cat

Proof

Step Hyp Ref Expression
1 df-oppc 
 |-  oppCat = ( f e. _V |-> ( ( f sSet <. ( Hom ` ndx ) , tpos ( Hom ` f ) >. ) sSet <. ( comp ` ndx ) , ( u e. ( ( Base ` f ) X. ( Base ` f ) ) , z e. ( Base ` f ) |-> tpos ( <. z , ( 2nd ` u ) >. ( comp ` f ) ( 1st ` u ) ) ) >. ) )
2 1 funmpt2 
 |-  Fun oppCat
3 ffvresb 
 |-  ( Fun oppCat -> ( ( oppCat |` Cat ) : Cat --> Cat <-> A. c e. Cat ( c e. dom oppCat /\ ( oppCat ` c ) e. Cat ) ) )
4 2 3 ax-mp 
 |-  ( ( oppCat |` Cat ) : Cat --> Cat <-> A. c e. Cat ( c e. dom oppCat /\ ( oppCat ` c ) e. Cat ) )
5 elex 
 |-  ( c e. Cat -> c e. _V )
6 ovex 
 |-  ( ( f sSet <. ( Hom ` ndx ) , tpos ( Hom ` f ) >. ) sSet <. ( comp ` ndx ) , ( u e. ( ( Base ` f ) X. ( Base ` f ) ) , z e. ( Base ` f ) |-> tpos ( <. z , ( 2nd ` u ) >. ( comp ` f ) ( 1st ` u ) ) ) >. ) e. _V
7 6 1 dmmpti 
 |-  dom oppCat = _V
8 5 7 eleqtrrdi 
 |-  ( c e. Cat -> c e. dom oppCat )
9 eqid 
 |-  ( oppCat ` c ) = ( oppCat ` c )
10 9 oppccat 
 |-  ( c e. Cat -> ( oppCat ` c ) e. Cat )
11 8 10 jca 
 |-  ( c e. Cat -> ( c e. dom oppCat /\ ( oppCat ` c ) e. Cat ) )
12 4 11 mprgbir 
 |-  ( oppCat |` Cat ) : Cat --> Cat