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

Metamath Proof Explorer

Theorem invisoinvr

Description: The inverse of an isomorphism is invers to the isomorphism. (Contributed by AV, 9-Apr-2020)

Ref Expression
Hypotheses invisoinv.b ⊢ B = Base C
invisoinv.i ⊢ I = Iso ⁡ C
invisoinv.n ⊢ N = Inv ⁡ C
invisoinv.c ⊢ φ → C ∈ Cat
invisoinv.x ⊢ φ → X ∈ B
invisoinv.y ⊢ φ → Y ∈ B
invisoinv.f ⊢ φ → F ∈ X I Y
Assertion invisoinvr ⊢ φ → F X N Y X N Y ⁡ F

Proof

Step Hyp Ref Expression
1 invisoinv.b ⊢ B = Base C
2 invisoinv.i ⊢ I = Iso ⁡ C
3 invisoinv.n ⊢ N = Inv ⁡ C
4 invisoinv.c ⊢ φ → C ∈ Cat
5 invisoinv.x ⊢ φ → X ∈ B
6 invisoinv.y ⊢ φ → Y ∈ B
7 invisoinv.f ⊢ φ → F ∈ X I Y
8 1 2 3 4 5 6 7 invisoinvl ⊢ φ → X N Y ⁡ F Y N X F
9 1 3 4 5 6 invsym ⊢ φ → F X N Y X N Y ⁡ F ↔ X N Y ⁡ F Y N X F
10 8 9 mpbird ⊢ φ → F X N Y X N Y ⁡ F