Database
BASIC CATEGORY THEORY
Categories
Sections, inverses, isomorphisms
sectid
Next ⟩
invid
Metamath Proof Explorer
Ascii
Unicode
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