Metamath Proof Explorer


Theorem sectfval

Description: Value of the section relation. (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 sectfval φ X S Y = f 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 7 sectffval φ S = x B , y B f g | f x H y g y H x g x y · ˙ x f = 1 ˙ x
10 simprl φ x = X y = Y x = X
11 simprr φ x = X y = Y y = Y
12 10 11 oveq12d φ x = X y = Y x H y = X H Y
13 12 eleq2d φ x = X y = Y f x H y f X H Y
14 11 10 oveq12d φ x = X y = Y y H x = Y H X
15 14 eleq2d φ x = X y = Y g y H x g Y H X
16 13 15 anbi12d φ x = X y = Y f x H y g y H x f X H Y g Y H X
17 10 11 opeq12d φ x = X y = Y x y = X Y
18 17 10 oveq12d φ x = X y = Y x y · ˙ x = X Y · ˙ X
19 18 oveqd φ x = X y = Y g x y · ˙ x f = g X Y · ˙ X f
20 10 fveq2d φ x = X y = Y 1 ˙ x = 1 ˙ X
21 19 20 eqeq12d φ x = X y = Y g x y · ˙ x f = 1 ˙ x g X Y · ˙ X f = 1 ˙ X
22 16 21 anbi12d φ x = X y = Y 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
23 22 opabbidv φ x = X y = Y 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
24 ovex X H Y V
25 ovex Y H X V
26 24 25 xpex X H Y × Y H X V
27 opabssxp f g | f X H Y g Y H X g X Y · ˙ X f = 1 ˙ X X H Y × Y H X
28 26 27 ssexi f g | f X H Y g Y H X g X Y · ˙ X f = 1 ˙ X V
29 28 a1i φ f g | f X H Y g Y H X g X Y · ˙ X f = 1 ˙ X V
30 9 23 7 8 29 ovmpod φ X S Y = f g | f X H Y g Y H X g X Y · ˙ X f = 1 ˙ X