Metamath Proof Explorer

Theorem oppcthinco

Description: If the opposite category of a thin category has the same base and hom-sets as the original category, then it has the same composition operation as the original category. (Contributed by Zhi Wang, 16-Oct-2025)

Ref Expression
Hypotheses oppcthinco.o ⊢ O = oppCat ⁡ C
oppcthinco.c ⊢ φ → C ∈ ThinCat
oppcthinco.1 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ O
Assertion oppcthinco ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ O

Proof

Step Hyp Ref Expression
1 oppcthinco.o ⊢ O = oppCat ⁡ C
2 oppcthinco.c ⊢ φ → C ∈ ThinCat
3 oppcthinco.1 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ O
4 eqid ⊢ Base C = Base C
5 eqid ⊢ comp ⁡ C = comp ⁡ C
6 simplr1 ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → x ∈ Base C
7 simplr2 ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → y ∈ Base C
8 simplr3 ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → z ∈ Base C
9 4 5 1 6 7 8 oppcco ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → g x y comp ⁡ O z f = f z y comp ⁡ C x g
10 eqid ⊢ Hom ⁡ C = Hom ⁡ C
11 2 ad2antrr ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → C ∈ ThinCat
12 11 thinccatd ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → C ∈ Cat
13 simprr ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → g ∈ y Hom ⁡ C z
14 eqid ⊢ Hom ⁡ O = Hom ⁡ O
15 3 ad2antrr ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ O
16 4 10 14 15 7 8 homfeqval ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → y Hom ⁡ C z = y Hom ⁡ O z
17 10 1 oppchom ⊢ y Hom ⁡ O z = z Hom ⁡ C y
18 16 17 eqtrdi ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → y Hom ⁡ C z = z Hom ⁡ C y
19 13 18 eleqtrd ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → g ∈ z Hom ⁡ C y
20 simprl ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → f ∈ x Hom ⁡ C y
21 4 10 14 15 6 7 homfeqval ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → x Hom ⁡ C y = x Hom ⁡ O y
22 10 1 oppchom ⊢ x Hom ⁡ O y = y Hom ⁡ C x
23 21 22 eqtrdi ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → x Hom ⁡ C y = y Hom ⁡ C x
24 20 23 eleqtrd ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → f ∈ y Hom ⁡ C x
25 4 10 5 12 8 7 6 19 24 catcocl ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → f z y comp ⁡ C x g ∈ z Hom ⁡ C x
26 4 10 14 15 6 8 homfeqval ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → x Hom ⁡ C z = x Hom ⁡ O z
27 10 1 oppchom ⊢ x Hom ⁡ O z = z Hom ⁡ C x
28 26 27 eqtrdi ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → x Hom ⁡ C z = z Hom ⁡ C x
29 25 28 eleqtrrd ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → f z y comp ⁡ C x g ∈ x Hom ⁡ C z
30 4 10 5 12 6 7 8 20 13 catcocl ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → g x y comp ⁡ C z f ∈ x Hom ⁡ C z
31 6 8 29 30 4 10 11 thincmo2 ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → f z y comp ⁡ C x g = g x y comp ⁡ C z f
32 9 31 eqtr2d ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → g x y comp ⁡ C z f = g x y comp ⁡ O z f
33 32 ralrimivva ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C → ∀ f ∈ x Hom ⁡ C y ∀ g ∈ y Hom ⁡ C z g x y comp ⁡ C z f = g x y comp ⁡ O z f
34 33 ralrimivvva ⊢ φ → ∀ x ∈ Base C ∀ y ∈ Base C ∀ z ∈ Base C ∀ f ∈ x Hom ⁡ C y ∀ g ∈ y Hom ⁡ C z g x y comp ⁡ C z f = g x y comp ⁡ O z f
35 eqid ⊢ comp ⁡ O = comp ⁡ O
36 eqidd ⊢ φ → Base C = Base C
37 3 homfeqbas ⊢ φ → Base C = Base O
38 5 35 10 36 37 3 comfeq ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ O ↔ ∀ x ∈ Base C ∀ y ∈ Base C ∀ z ∈ Base C ∀ f ∈ x Hom ⁡ C y ∀ g ∈ y Hom ⁡ C z g x y comp ⁡ C z f = g x y comp ⁡ O z f
39 34 38 mpbird ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ O