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

Definition df-oppc 16366
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 16365 . 2 class oppCat
2 vf . . 3 setvar 𝑓
3 cvv 3198 . . 3 class V
42cv 1481 . . . . 5 class 𝑓
5 cnx 15848 . . . . . . 7 class ndx
6 chom 15946 . . . . . . 7 class Hom
75, 6cfv 5886 . . . . . 6 class (Hom ‘ndx)
84, 6cfv 5886 . . . . . . 7 class (Hom ‘𝑓)
98ctpos 7348 . . . . . 6 class tpos (Hom ‘𝑓)
107, 9cop 4181 . . . . 5 class ⟨(Hom ‘ndx), tpos (Hom ‘𝑓)⟩
11 csts 15849 . . . . 5 class sSet
124, 10, 11co 6647 . . . 4 class (𝑓 sSet ⟨(Hom ‘ndx), tpos (Hom ‘𝑓)⟩)
13 cco 15947 . . . . . 6 class comp
145, 13cfv 5886 . . . . 5 class (comp‘ndx)
15 vu . . . . . 6 setvar 𝑢
16 vz . . . . . 6 setvar 𝑧
17 cbs 15851 . . . . . . . 8 class Base
184, 17cfv 5886 . . . . . . 7 class (Base‘𝑓)
1918, 18cxp 5110 . . . . . 6 class ((Base‘𝑓) × (Base‘𝑓))
2016cv 1481 . . . . . . . . 9 class 𝑧
2115cv 1481 . . . . . . . . . 10 class 𝑢
22 c2nd 7164 . . . . . . . . . 10 class 2nd
2321, 22cfv 5886 . . . . . . . . 9 class (2nd𝑢)
2420, 23cop 4181 . . . . . . . 8 class 𝑧, (2nd𝑢)⟩
25 c1st 7163 . . . . . . . . 9 class 1st
2621, 25cfv 5886 . . . . . . . 8 class (1st𝑢)
274, 13cfv 5886 . . . . . . . 8 class (comp‘𝑓)
2824, 26, 27co 6647 . . . . . . 7 class (⟨𝑧, (2nd𝑢)⟩(comp‘𝑓)(1st𝑢))
2928ctpos 7348 . . . . . 6 class tpos (⟨𝑧, (2nd𝑢)⟩(comp‘𝑓)(1st𝑢))
3015, 16, 19, 18, 29cmpt2 6649 . . . . 5 class (𝑢 ∈ ((Base‘𝑓) × (Base‘𝑓)), 𝑧 ∈ (Base‘𝑓) ↦ tpos (⟨𝑧, (2nd𝑢)⟩(comp‘𝑓)(1st𝑢)))
3114, 30cop 4181 . . . 4 class ⟨(comp‘ndx), (𝑢 ∈ ((Base‘𝑓) × (Base‘𝑓)), 𝑧 ∈ (Base‘𝑓) ↦ tpos (⟨𝑧, (2nd𝑢)⟩(comp‘𝑓)(1st𝑢)))⟩
3212, 31, 11co 6647 . . 3 class ((𝑓 sSet ⟨(Hom ‘ndx), tpos (Hom ‘𝑓)⟩) sSet ⟨(comp‘ndx), (𝑢 ∈ ((Base‘𝑓) × (Base‘𝑓)), 𝑧 ∈ (Base‘𝑓) ↦ tpos (⟨𝑧, (2nd𝑢)⟩(comp‘𝑓)(1st𝑢)))⟩)
332, 3, 32cmpt 4727 . 2 class (𝑓 ∈ V ↦ ((𝑓 sSet ⟨(Hom ‘ndx), tpos (Hom ‘𝑓)⟩) sSet ⟨(comp‘ndx), (𝑢 ∈ ((Base‘𝑓) × (Base‘𝑓)), 𝑧 ∈ (Base‘𝑓) ↦ tpos (⟨𝑧, (2nd𝑢)⟩(comp‘𝑓)(1st𝑢)))⟩))
341, 33wceq 1482 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  16367
  Copyright terms: Public domain W3C validator