Database
BASIC CATEGORY THEORY
Categories
Sections, inverses, isomorphisms
invid
Next ⟩
idiso
Metamath Proof Explorer
Ascii
Unicode
Theorem
invid
Description:
The inverse of the identity is the identity.
(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
invid
⊢
φ
→
I
⁡
X
X
Inv
⁡
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
1
2
3
4
sectid
⊢
φ
→
I
⁡
X
X
Sect
⁡
C
X
I
⁡
X
6
eqid
⊢
Inv
⁡
C
=
Inv
⁡
C
7
eqid
⊢
Sect
⁡
C
=
Sect
⁡
C
8
1
6
3
4
4
7
isinv
⊢
φ
→
I
⁡
X
X
Inv
⁡
C
X
I
⁡
X
↔
I
⁡
X
X
Sect
⁡
C
X
I
⁡
X
∧
I
⁡
X
X
Sect
⁡
C
X
I
⁡
X
9
5
5
8
mpbir2and
⊢
φ
→
I
⁡
X
X
Inv
⁡
C
X
I
⁡
X