invcoisoid

Description: The inverse of an isomorphism composed with the isomorphism is the identity. (Contributed by AV, 5-Apr-2020)

	Ref	Expression
Hypotheses	invisoinv.b	$⊢ B = {Base}_{C}$
	invisoinv.i	$⊢ I = Iso (C)$
	invisoinv.n	$⊢ N = Inv (C)$
	invisoinv.c	$⊢ φ \to C \in Cat$
	invisoinv.x	$⊢ φ \to X \in B$
	invisoinv.y	$⊢ φ \to Y \in B$
	invisoinv.f	$⊢ φ \to F \in (X I Y)$
	invcoisoid.1	$⊢ \underset{˙}{1} = Id (C)$
	invcoisoid.o	No typesetting found for \|- .o. = ( <. X , Y >. ( comp ` C ) X ) with typecode \|-
Assertion	invcoisoid	Could not format assertion : No typesetting found for \|- ( ph -> ( ( ( X N Y ) ` F ) .o. F ) = ( .1. ` X ) ) with typecode \|-

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	$⊢ φ \to C \in Cat$
5		invisoinv.x	$⊢ φ \to X \in B$
6		invisoinv.y	$⊢ φ \to Y \in B$
7		invisoinv.f	$⊢ φ \to F \in (X I Y)$
8		invcoisoid.1	$⊢ \underset{˙}{1} = Id (C)$
9		invcoisoid.o	Could not format .o. = ( <. X , Y >. ( comp ` C ) X ) : No typesetting found for \|- .o. = ( <. X , Y >. ( comp ` C ) X ) with typecode \|-
10	1 2 3 4 5 6 7	invisoinvr	$⊢ φ \to F (X N Y) (X N Y) (F)$
11		eqid	$⊢ Sect (C) = Sect (C)$
12	1 3 4 5 6 11	isinv	$⊢ φ \to (F (X N Y) (X N Y) (F) \leftrightarrow (F (X Sect (C) Y) (X N Y) (F) \land (X N Y) (F) (Y Sect (C) X) F))$
13		simpl	$⊢ (F (X Sect (C) Y) (X N Y) (F) \land (X N Y) (F) (Y Sect (C) X) F) \to F (X Sect (C) Y) (X N Y) (F)$
14	12 13	biimtrdi	$⊢ φ \to (F (X N Y) (X N Y) (F) \to F (X Sect (C) Y) (X N Y) (F))$
15	10 14	mpd	$⊢ φ \to F (X Sect (C) Y) (X N Y) (F)$
16		eqid	$⊢ Hom (C) = Hom (C)$
17		eqid	$⊢ comp (C) = comp (C)$
18	1 16 2 4 5 6	isohom	$⊢ φ \to X I Y \subseteq X Hom (C) Y$
19	18 7	sseldd	$⊢ φ \to F \in (X Hom (C) Y)$
20	1 16 2 4 6 5	isohom	$⊢ φ \to Y I X \subseteq Y Hom (C) X$
21	1 3 4 5 6 2	invf	$⊢ φ \to (X N Y) : X I Y ⟶ Y I X$
22	21 7	ffvelcdmd	$⊢ φ \to (X N Y) (F) \in (Y I X)$
23	20 22	sseldd	$⊢ φ \to (X N Y) (F) \in (Y Hom (C) X)$
24	1 16 17 8 11 4 5 6 19 23	issect2	$⊢ φ \to (F (X Sect (C) Y) (X N Y) (F) \leftrightarrow (X N Y) (F) (⟨X, Y⟩ comp (C) X) F = \underset{˙}{1} (X))$
25	9	a1i	Could not format ( ph -> .o. = ( <. X , Y >. ( comp ` C ) X ) ) : No typesetting found for \|- ( ph -> .o. = ( <. X , Y >. ( comp ` C ) X ) ) with typecode \|-
26	25	eqcomd	Could not format ( ph -> ( <. X , Y >. ( comp ` C ) X ) = .o. ) : No typesetting found for \|- ( ph -> ( <. X , Y >. ( comp ` C ) X ) = .o. ) with typecode \|-
27	26	oveqd	Could not format ( ph -> ( ( ( X N Y ) ` F ) ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( ( X N Y ) ` F ) .o. F ) ) : No typesetting found for \|- ( ph -> ( ( ( X N Y ) ` F ) ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( ( X N Y ) ` F ) .o. F ) ) with typecode \|-
28	27	eqeq1d	Could not format ( ph -> ( ( ( ( X N Y ) ` F ) ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) <-> ( ( ( X N Y ) ` F ) .o. F ) = ( .1. ` X ) ) ) : No typesetting found for \|- ( ph -> ( ( ( ( X N Y ) ` F ) ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) <-> ( ( ( X N Y ) ` F ) .o. F ) = ( .1. ` X ) ) ) with typecode \|-
29	24 28	bitrd	Could not format ( ph -> ( F ( X ( Sect ` C ) Y ) ( ( X N Y ) ` F ) <-> ( ( ( X N Y ) ` F ) .o. F ) = ( .1. ` X ) ) ) : No typesetting found for \|- ( ph -> ( F ( X ( Sect ` C ) Y ) ( ( X N Y ) ` F ) <-> ( ( ( X N Y ) ` F ) .o. F ) = ( .1. ` X ) ) ) with typecode \|-
30	15 29	mpbid	Could not format ( ph -> ( ( ( X N Y ) ` F ) .o. F ) = ( .1. ` X ) ) : No typesetting found for \|- ( ph -> ( ( ( X N Y ) ` F ) .o. F ) = ( .1. ` X ) ) with typecode \|-

Metamath Proof Explorer

Theorem invcoisoid

Proof