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 V f sSet Hom ndx tpos Hom f sSet comp ndx u Base f × Base f , z Base f tpos z 2 nd u comp f 1 st u
2 1 funmpt2 Fun oppCat
3 ffvresb Fun oppCat oppCat Cat : Cat Cat c Cat c dom oppCat oppCat c Cat
4 2 3 ax-mp oppCat Cat : Cat Cat c Cat c dom oppCat oppCat c Cat
5 elex c Cat c V
6 ovex f sSet Hom ndx tpos Hom f sSet comp ndx u Base f × Base f , z Base f tpos z 2 nd u comp f 1 st u V
7 6 1 dmmpti dom oppCat = V
8 5 7 eleqtrrdi c Cat c dom oppCat
9 eqid oppCat c = oppCat c
10 9 oppccat c Cat oppCat c Cat
11 8 10 jca c Cat c dom oppCat oppCat c Cat
12 4 11 mprgbir oppCat Cat : Cat Cat