This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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