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

Metamath Proof Explorer

Theorem idiso

Description: The identity is an isomorphism. Example 3.13 of Adamek p. 28. (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 idiso ⊢ φ → I ⁡ X ∈ X Iso ⁡ C 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 ⊢ Inv ⁡ C = Inv ⁡ C
6 eqid ⊢ Iso ⁡ C = Iso ⁡ C
7 1 2 3 4 invid ⊢ φ → I ⁡ X X Inv ⁡ C X I ⁡ X
8 1 5 3 4 4 6 7 inviso1 ⊢ φ → I ⁡ X ∈ X Iso ⁡ C X