Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-oppc Structured version   Visualization version   GIF version

Definition df-oppc 16961
 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
StepHypRef Expression
1 coppc 16960 . 2 class oppCat
2 vf . . 3 setvar 𝑓
3 cvv 3473 . . 3 class V
42cv 1536 . . . . 5 class 𝑓
5 cnx 16459 . . . . . . 7 class ndx
6 chom 16555 . . . . . . 7 class Hom
75, 6cfv 6331 . . . . . 6 class (Hom ‘ndx)
84, 6cfv 6331 . . . . . . 7 class (Hom ‘𝑓)
98ctpos 7869 . . . . . 6 class tpos (Hom ‘𝑓)
107, 9cop 4549 . . . . 5 class ⟨(Hom ‘ndx), tpos (Hom ‘𝑓)⟩
11 csts 16460 . . . . 5 class sSet
124, 10, 11co 7133 . . . 4 class (𝑓 sSet ⟨(Hom ‘ndx), tpos (Hom ‘𝑓)⟩)
13 cco 16556 . . . . . 6 class comp
145, 13cfv 6331 . . . . 5 class (comp‘ndx)
15 vu . . . . . 6 setvar 𝑢
16 vz . . . . . 6 setvar 𝑧
17 cbs 16462 . . . . . . . 8 class Base
184, 17cfv 6331 . . . . . . 7 class (Base‘𝑓)
1918, 18cxp 5529 . . . . . 6 class ((Base‘𝑓) × (Base‘𝑓))
2016cv 1536 . . . . . . . . 9 class 𝑧
2115cv 1536 . . . . . . . . . 10 class 𝑢
22 c2nd 7666 . . . . . . . . . 10 class 2nd
2321, 22cfv 6331 . . . . . . . . 9 class (2nd𝑢)
2420, 23cop 4549 . . . . . . . 8 class 𝑧, (2nd𝑢)⟩
25 c1st 7665 . . . . . . . . 9 class 1st
2621, 25cfv 6331 . . . . . . . 8 class (1st𝑢)
274, 13cfv 6331 . . . . . . . 8 class (comp‘𝑓)
2824, 26, 27co 7133 . . . . . . 7 class (⟨𝑧, (2nd𝑢)⟩(comp‘𝑓)(1st𝑢))
2928ctpos 7869 . . . . . 6 class tpos (⟨𝑧, (2nd𝑢)⟩(comp‘𝑓)(1st𝑢))
3015, 16, 19, 18, 29cmpo 7135 . . . . 5 class (𝑢 ∈ ((Base‘𝑓) × (Base‘𝑓)), 𝑧 ∈ (Base‘𝑓) ↦ tpos (⟨𝑧, (2nd𝑢)⟩(comp‘𝑓)(1st𝑢)))
3114, 30cop 4549 . . . 4 class ⟨(comp‘ndx), (𝑢 ∈ ((Base‘𝑓) × (Base‘𝑓)), 𝑧 ∈ (Base‘𝑓) ↦ tpos (⟨𝑧, (2nd𝑢)⟩(comp‘𝑓)(1st𝑢)))⟩
3212, 31, 11co 7133 . . 3 class ((𝑓 sSet ⟨(Hom ‘ndx), tpos (Hom ‘𝑓)⟩) sSet ⟨(comp‘ndx), (𝑢 ∈ ((Base‘𝑓) × (Base‘𝑓)), 𝑧 ∈ (Base‘𝑓) ↦ tpos (⟨𝑧, (2nd𝑢)⟩(comp‘𝑓)(1st𝑢)))⟩)
332, 3, 32cmpt 5122 . 2 class (𝑓 ∈ V ↦ ((𝑓 sSet ⟨(Hom ‘ndx), tpos (Hom ‘𝑓)⟩) sSet ⟨(comp‘ndx), (𝑢 ∈ ((Base‘𝑓) × (Base‘𝑓)), 𝑧 ∈ (Base‘𝑓) ↦ tpos (⟨𝑧, (2nd𝑢)⟩(comp‘𝑓)(1st𝑢)))⟩))
341, 33wceq 1537 1 wff oppCat = (𝑓 ∈ V ↦ ((𝑓 sSet ⟨(Hom ‘ndx), tpos (Hom ‘𝑓)⟩) sSet ⟨(comp‘ndx), (𝑢 ∈ ((Base‘𝑓) × (Base‘𝑓)), 𝑧 ∈ (Base‘𝑓) ↦ tpos (⟨𝑧, (2nd𝑢)⟩(comp‘𝑓)(1st𝑢)))⟩))
 Colors of variables: wff setvar class This definition is referenced by:  oppcval  16962
 Copyright terms: Public domain W3C validator