Metamath Proof Explorer


Theorem sectss

Description: The section relation is a relation between morphisms from X to Y and morphisms from Y to X . (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses issect.b B=BaseC
issect.h H=HomC
issect.o ·˙=compC
issect.i 1˙=IdC
issect.s S=SectC
issect.c φCCat
issect.x φXB
issect.y φYB
Assertion sectss φXSYXHY×YHX

Proof

Step Hyp Ref Expression
1 issect.b B=BaseC
2 issect.h H=HomC
3 issect.o ·˙=compC
4 issect.i 1˙=IdC
5 issect.s S=SectC
6 issect.c φCCat
7 issect.x φXB
8 issect.y φYB
9 1 2 3 4 5 6 7 8 sectfval φXSY=fg|fXHYgYHXgXY·˙Xf=1˙X
10 opabssxp fg|fXHYgYHXgXY·˙Xf=1˙XXHY×YHX
11 9 10 eqsstrdi φXSYXHY×YHX