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