Metamath Proof Explorer


Theorem sectid

Description: The identity is a section of itself. (Contributed by AV, 8-Apr-2020)

Ref Expression
Hypotheses invid.b B = Base C
invid.i I = Id C
invid.c φ C Cat
invid.x φ X B
Assertion sectid φ I X X Sect C X I X

Proof

Step Hyp Ref Expression
1 invid.b B = Base C
2 invid.i I = Id C
3 invid.c φ C Cat
4 invid.x φ X B
5 eqid Hom C = Hom C
6 eqid comp C = comp C
7 1 5 2 3 4 catidcl φ I X X Hom C X
8 1 5 2 3 4 6 4 7 catlid φ I X X X comp C X I X = I X
9 eqid Sect C = Sect C
10 1 5 6 2 9 3 4 4 7 7 issect2 φ I X X Sect C X I X I X X X comp C X I X = I X
11 8 10 mpbird φ I X X Sect C X I X