Metamath Proof Explorer

Theorem oppcsect2

Description: A section in the opposite category. (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
oppcsect.s ⊢ S = Sect ⁡ C
oppcsect.t ⊢ T = Sect ⁡ O
Assertion oppcsect2 ⊢ φ → X T Y = X S Y -1

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 oppcsect.s ⊢ S = Sect ⁡ C
7 oppcsect.t ⊢ T = Sect ⁡ O
8 2 1 oppcbas ⊢ B = Base O
9 eqid ⊢ Hom ⁡ O = Hom ⁡ O
10 eqid ⊢ comp ⁡ O = comp ⁡ O
11 eqid ⊢ Id ⁡ O = Id ⁡ O
12 2 oppccat ⊢ C ∈ Cat → O ∈ Cat
13 3 12 syl ⊢ φ → O ∈ Cat
14 8 9 10 11 7 13 4 5 sectss ⊢ φ → X T Y ⊆ X Hom ⁡ O Y × Y Hom ⁡ O X
15 relxp ⊢ Rel ⁡ X Hom ⁡ O Y × Y Hom ⁡ O X
16 relss ⊢ X T Y ⊆ X Hom ⁡ O Y × Y Hom ⁡ O X → Rel ⁡ X Hom ⁡ O Y × Y Hom ⁡ O X → Rel ⁡ X T Y
17 14 15 16 mpisyl ⊢ φ → Rel ⁡ X T Y
18 relcnv ⊢ Rel ⁡ X S Y -1
19 18 a1i ⊢ φ → Rel ⁡ X S Y -1
20 1 2 3 4 5 6 7 oppcsect ⊢ φ → f X T Y g ↔ g X S Y f
21 vex ⊢ f ∈ V
22 vex ⊢ g ∈ V
23 21 22 brcnv ⊢ f X S Y -1 g ↔ g X S Y f
24 20 23 bitr4di ⊢ φ → f X T Y g ↔ f X S Y -1 g
25 17 19 24 eqbrrdv ⊢ φ → X T Y = X S Y -1