Metamath Proof Explorer

Definition df-oppc

Description: Define an opposite category, which is the same as the original category but with the direction of arrows the other way around. Definition 3.5 of Adamek p. 25. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion 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

Detailed syntax breakdown

Step Hyp Ref Expression
0 coppc class oppCat
1 vf setvar f
2 cvv class V
3 1 cv setvar f
4 csts class sSet
5 chom class Hom
6 cnx class ndx
7 6 5 cfv class Hom ⁡ ndx
8 3 5 cfv class Hom ⁡ f
9 8 ctpos class tpos Hom ⁡ f
10 7 9 cop class Hom ⁡ ndx tpos Hom ⁡ f
11 3 10 4 co class f sSet Hom ⁡ ndx tpos Hom ⁡ f
12 cco class comp
13 6 12 cfv class comp ⁡ ndx
14 vu setvar u
15 cbs class Base
16 3 15 cfv class Base f
17 16 16 cxp class Base f × Base f
18 vz setvar z
19 18 cv setvar z
20 c2nd class 2 nd
21 14 cv setvar u
22 21 20 cfv class 2 nd ⁡ u
23 19 22 cop class z 2 nd ⁡ u
24 3 12 cfv class comp ⁡ f
25 c1st class 1 st
26 21 25 cfv class 1 st ⁡ u
27 23 26 24 co class z 2 nd ⁡ u comp ⁡ f 1 st ⁡ u
28 27 ctpos class tpos z 2 nd ⁡ u comp ⁡ f 1 st ⁡ u
29 14 18 17 16 28 cmpo class u ∈ Base f × Base f , z ∈ Base f ⟼ tpos z 2 nd ⁡ u comp ⁡ f 1 st ⁡ u
30 13 29 cop class comp ⁡ ndx u ∈ Base f × Base f , z ∈ Base f ⟼ tpos z 2 nd ⁡ u comp ⁡ f 1 st ⁡ u
31 11 30 4 co class 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
32 1 2 31 cmpt class 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
33 0 32 wceq wff 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