Metamath Proof Explorer


Theorem issect2

Description: Property of being a section. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses issect.b B = Base C
issect.h H = Hom C
issect.o · ˙ = comp C
issect.i 1 ˙ = Id C
issect.s S = Sect C
issect.c φ C Cat
issect.x φ X B
issect.y φ Y B
issect.f φ F X H Y
issect.g φ G Y H X
Assertion issect2 φ F X S Y G G X Y · ˙ X F = 1 ˙ X

Proof

Step Hyp Ref Expression
1 issect.b B = Base C
2 issect.h H = Hom C
3 issect.o · ˙ = comp C
4 issect.i 1 ˙ = Id C
5 issect.s S = Sect C
6 issect.c φ C Cat
7 issect.x φ X B
8 issect.y φ Y B
9 issect.f φ F X H Y
10 issect.g φ G Y H X
11 9 10 jca φ F X H Y G Y H X
12 1 2 3 4 5 6 7 8 issect φ F X S Y G F X H Y G Y H X G X Y · ˙ X F = 1 ˙ X
13 df-3an F X H Y G Y H X G X Y · ˙ X F = 1 ˙ X F X H Y G Y H X G X Y · ˙ X F = 1 ˙ X
14 12 13 bitrdi φ F X S Y G F X H Y G Y H X G X Y · ˙ X F = 1 ˙ X
15 11 14 mpbirand φ F X S Y G G X Y · ˙ X F = 1 ˙ X