This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oppciso

Description: An isomorphism in the opposite category. See also remark 3.9 in Adamek p. 28. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses oppcsect.b ⊢ B = Base C
oppcsect.o ⊢ O = oppCat ⁡ C
oppcsect.c ⊢ φ → C ∈ Cat
oppcsect.x ⊢ φ → X ∈ B
oppcsect.y ⊢ φ → Y ∈ B
oppciso.s ⊢ I = Iso ⁡ C
oppciso.t ⊢ J = Iso ⁡ O
Assertion oppciso ⊢ φ → X J Y = Y I X

Proof

Step Hyp Ref Expression
1 oppcsect.b ⊢ B = Base C
2 oppcsect.o ⊢ O = oppCat ⁡ C
3 oppcsect.c ⊢ φ → C ∈ Cat
4 oppcsect.x ⊢ φ → X ∈ B
5 oppcsect.y ⊢ φ → Y ∈ B
6 oppciso.s ⊢ I = Iso ⁡ C
7 oppciso.t ⊢ J = Iso ⁡ O
8 eqid ⊢ Inv ⁡ C = Inv ⁡ C
9 eqid ⊢ Inv ⁡ O = Inv ⁡ O
10 1 2 3 4 5 8 9 oppcinv ⊢ φ → X Inv ⁡ O Y = Y Inv ⁡ C X
11 10 dmeqd ⊢ φ → dom ⁡ X Inv ⁡ O Y = dom ⁡ Y Inv ⁡ C X
12 2 1 oppcbas ⊢ B = Base O
13 2 oppccat ⊢ C ∈ Cat → O ∈ Cat
14 3 13 syl ⊢ φ → O ∈ Cat
15 12 9 14 4 5 7 isoval ⊢ φ → X J Y = dom ⁡ X Inv ⁡ O Y
16 1 8 3 5 4 6 isoval ⊢ φ → Y I X = dom ⁡ Y Inv ⁡ C X
17 11 15 16 3eqtr4d ⊢ φ → X J Y = Y I X