Definition df-oppc 17755

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.)

Assertion

Ref	Expression
df-oppc	⊢ oppCat = (𝑓 ∈ V ↦ ((𝑓 sSet ⟨(Hom ‘ndx), tpos (Hom ‘𝑓)⟩) sSet ⟨(comp‘ndx), (𝑢 ∈ ((Base‘𝑓) × (Base‘𝑓)), 𝑧 ∈ (Base‘𝑓) ↦ tpos (⟨𝑧, (2nd ‘𝑢)⟩(comp‘𝑓)(1st ‘𝑢)))⟩))

Distinct variable group:   𝑢,𝑓,𝑧

Detailed syntax breakdown of Definition df-oppc

Step	Hyp	Ref	Expression
1		coppc 17754	. 2 class oppCat
2		vf	. . 3 setvar 𝑓
3		cvv 3480	. . 3 class V
4	2	cv 1539	. . . . 5 class 𝑓
5		cnx 17230	. . . . . . 7 class ndx
6		chom 17308	. . . . . . 7 class Hom
7	5, 6	cfv 6561	. . . . . 6 class (Hom ‘ndx)
8	4, 6	cfv 6561	. . . . . . 7 class (Hom ‘𝑓)
9	8	ctpos 8250	. . . . . 6 class tpos (Hom ‘𝑓)
10	7, 9	cop 4632	. . . . 5 class ⟨(Hom ‘ndx), tpos (Hom ‘𝑓)⟩
11		csts 17200	. . . . 5 class sSet
12	4, 10, 11	co 7431	. . . 4 class (𝑓 sSet ⟨(Hom ‘ndx), tpos (Hom ‘𝑓)⟩)
13		cco 17309	. . . . . 6 class comp
14	5, 13	cfv 6561	. . . . 5 class (comp‘ndx)
15		vu	. . . . . 6 setvar 𝑢
16		vz	. . . . . 6 setvar 𝑧
17		cbs 17247	. . . . . . . 8 class Base
18	4, 17	cfv 6561	. . . . . . 7 class (Base‘𝑓)
19	18, 18	cxp 5683	. . . . . 6 class ((Base‘𝑓) × (Base‘𝑓))
20	16	cv 1539	. . . . . . . . 9 class 𝑧
21	15	cv 1539	. . . . . . . . . 10 class 𝑢
22		c2nd 8013	. . . . . . . . . 10 class 2nd
23	21, 22	cfv 6561	. . . . . . . . 9 class (2nd ‘𝑢)
24	20, 23	cop 4632	. . . . . . . 8 class ⟨𝑧, (2nd ‘𝑢)⟩
25		c1st 8012	. . . . . . . . 9 class 1st
26	21, 25	cfv 6561	. . . . . . . 8 class (1st ‘𝑢)
27	4, 13	cfv 6561	. . . . . . . 8 class (comp‘𝑓)
28	24, 26, 27	co 7431	. . . . . . 7 class (⟨𝑧, (2nd ‘𝑢)⟩(comp‘𝑓)(1st ‘𝑢))
29	28	ctpos 8250	. . . . . 6 class tpos (⟨𝑧, (2nd ‘𝑢)⟩(comp‘𝑓)(1st ‘𝑢))
30	15, 16, 19, 18, 29	cmpo 7433	. . . . 5 class (𝑢 ∈ ((Base‘𝑓) × (Base‘𝑓)), 𝑧 ∈ (Base‘𝑓) ↦ tpos (⟨𝑧, (2nd ‘𝑢)⟩(comp‘𝑓)(1st ‘𝑢)))
31	14, 30	cop 4632	. . . 4 class ⟨(comp‘ndx), (𝑢 ∈ ((Base‘𝑓) × (Base‘𝑓)), 𝑧 ∈ (Base‘𝑓) ↦ tpos (⟨𝑧, (2nd ‘𝑢)⟩(comp‘𝑓)(1st ‘𝑢)))⟩
32	12, 31, 11	co 7431	. . 3 class ((𝑓 sSet ⟨(Hom ‘ndx), tpos (Hom ‘𝑓)⟩) sSet ⟨(comp‘ndx), (𝑢 ∈ ((Base‘𝑓) × (Base‘𝑓)), 𝑧 ∈ (Base‘𝑓) ↦ tpos (⟨𝑧, (2nd ‘𝑢)⟩(comp‘𝑓)(1st ‘𝑢)))⟩)
33	2, 3, 32	cmpt 5225	. 2 class (𝑓 ∈ V ↦ ((𝑓 sSet ⟨(Hom ‘ndx), tpos (Hom ‘𝑓)⟩) sSet ⟨(comp‘ndx), (𝑢 ∈ ((Base‘𝑓) × (Base‘𝑓)), 𝑧 ∈ (Base‘𝑓) ↦ tpos (⟨𝑧, (2nd ‘𝑢)⟩(comp‘𝑓)(1st ‘𝑢)))⟩))
34	1, 33	wceq 1540	1 wff oppCat = (𝑓 ∈ V ↦ ((𝑓 sSet ⟨(Hom ‘ndx), tpos (Hom ‘𝑓)⟩) sSet ⟨(comp‘ndx), (𝑢 ∈ ((Base‘𝑓) × (Base‘𝑓)), 𝑧 ∈ (Base‘𝑓) ↦ tpos (⟨𝑧, (2nd ‘𝑢)⟩(comp‘𝑓)(1st ‘𝑢)))⟩))

This definition is referenced by:  oppcval  17756  oppccatf  17771