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

Metamath Proof Explorer

Theorem invinv

Description: The inverse of the inverse of an isomorphism is itself. Proposition 3.14(1) of Adamek p. 29. (Contributed by Mario Carneiro, 2-Jan-2017)

		Ref	Expression
	Hypotheses	invfval.b	$⊢ B = {Base}_{C}$
		invfval.n	$⊢ N = Inv (C)$
		invfval.c	$⊢ φ \to C \in Cat$
		invss.x	$⊢ φ \to X \in B$
		invss.y	$⊢ φ \to Y \in B$
		isoval.n	$⊢ I = Iso (C)$
		invinv.f	$⊢ φ \to F \in (X I Y)$
	Assertion	invinv	$⊢ φ \to (Y N X) ((X N Y) (F)) = F$

Proof

Step	Hyp	Ref	Expression
1		invfval.b	$⊢ B = {Base}_{C}$
2		invfval.n	$⊢ N = Inv (C)$
3		invfval.c	$⊢ φ \to C \in Cat$
4		invss.x	$⊢ φ \to X \in B$
5		invss.y	$⊢ φ \to Y \in B$
6		isoval.n	$⊢ I = Iso (C)$
7		invinv.f	$⊢ φ \to F \in (X I Y)$
8	1 2 3 4 5	invsym2	$⊢ φ \to {(X N Y)}^{-1} = Y N X$
9	8	fveq1d	$⊢ φ \to {(X N Y)}^{-1} ((X N Y) (F)) = (Y N X) ((X N Y) (F))$
10	1 2 3 4 5 6	invf1o	$⊢ φ \to (X N Y) : X I Y \underset{1-1 onto}{⟶} Y I X$
11		f1ocnvfv1	$⊢ ((X N Y) : X I Y \underset{1-1 onto}{⟶} Y I X \land F \in (X I Y)) \to {(X N Y)}^{-1} ((X N Y) (F)) = F$
12	10 7 11	syl2anc	$⊢ φ \to {(X N Y)}^{-1} ((X N Y) (F)) = F$
13	9 12	eqtr3d	$⊢ φ \to (Y N X) ((X N Y) (F)) = F$