Metamath Proof Explorer


Theorem issect

Description: The property " F is a section of G ". (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
Assertion issect φ F X S Y G F X H Y G Y H X 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 1 2 3 4 5 6 7 8 sectfval φ X S Y = f g | f X H Y g Y H X g X Y · ˙ X f = 1 ˙ X
10 9 breqd φ F X S Y G F f g | f X H Y g Y H X g X Y · ˙ X f = 1 ˙ X G
11 oveq12 g = G f = F g X Y · ˙ X f = G X Y · ˙ X F
12 11 ancoms f = F g = G g X Y · ˙ X f = G X Y · ˙ X F
13 12 eqeq1d f = F g = G g X Y · ˙ X f = 1 ˙ X G X Y · ˙ X F = 1 ˙ X
14 eqid f g | f X H Y g Y H X g X Y · ˙ X f = 1 ˙ X = f g | f X H Y g Y H X g X Y · ˙ X f = 1 ˙ X
15 13 14 brab2a F f g | f X H Y g Y H X g X Y · ˙ X f = 1 ˙ X G F X H Y G Y H X G X Y · ˙ X F = 1 ˙ X
16 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
17 15 16 bitr4i F f g | f X H Y g Y H X g X Y · ˙ X f = 1 ˙ X G F X H Y G Y H X G X Y · ˙ X F = 1 ˙ X
18 10 17 bitrdi φ F X S Y G F X H Y G Y H X G X Y · ˙ X F = 1 ˙ X