Theorem 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={\mathrm{Base}}_C$$
	invisoinv.i	$$⊢I=\mathrm{Iso}\left(C\right)$$
	invisoinv.n	$$⊢N=\mathrm{Inv}\left(C\right)$$
	invisoinv.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	invisoinv.x	$$⊢\phi \to X\in B$$
	invisoinv.y	$$⊢\phi \to Y\in B$$
	invisoinv.f	$$⊢\phi \to F\in \left(XIY\right)$$
	invcoisoid.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
	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={\mathrm{Base}}_C$$
2		invisoinv.i	$$⊢I=\mathrm{Iso}\left(C\right)$$
3		invisoinv.n	$$⊢N=\mathrm{Inv}\left(C\right)$$
4		invisoinv.c	$$⊢\phi \to C\in \mathrm{Cat}$$
5		invisoinv.x	$$⊢\phi \to X\in B$$
6		invisoinv.y	$$⊢\phi \to Y\in B$$
7		invisoinv.f	$$⊢\phi \to F\in \left(XIY\right)$$
8		invcoisoid.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
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	$$⊢\phi \to F\left(XNY\right)\left(XNY\right)\left(F\right)$$
11		eqid	$$⊢\mathrm{Sect}\left(C\right)=\mathrm{Sect}\left(C\right)$$
12	1 3 4 5 6 11	isinv	$$⊢\phi \to \left(F\left(XNY\right)\left(XNY\right)\left(F\right)\leftrightarrow \left(F\left(X\mathrm{Sect}\left(C\right)Y\right)\left(XNY\right)\left(F\right)\wedge \left(XNY\right)\left(F\right)\left(Y\mathrm{Sect}\left(C\right)X\right)F\right)\right)$$
13		simpl	$$⊢\left(F\left(X\mathrm{Sect}\left(C\right)Y\right)\left(XNY\right)\left(F\right)\wedge \left(XNY\right)\left(F\right)\left(Y\mathrm{Sect}\left(C\right)X\right)F\right)\to F\left(X\mathrm{Sect}\left(C\right)Y\right)\left(XNY\right)\left(F\right)$$
14	12 13	syl6bi	$$⊢\phi \to \left(F\left(XNY\right)\left(XNY\right)\left(F\right)\to F\left(X\mathrm{Sect}\left(C\right)Y\right)\left(XNY\right)\left(F\right)\right)$$
15	10 14	mpd	$$⊢\phi \to F\left(X\mathrm{Sect}\left(C\right)Y\right)\left(XNY\right)\left(F\right)$$
16		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
17		eqid	$$⊢\mathrm{comp}\left(C\right)=\mathrm{comp}\left(C\right)$$
18	1 16 2 4 5 6	isohom	$$⊢\phi \to XIY\subseteq X\mathrm{Hom}\left(C\right)Y$$
19	18 7	sseldd	$$⊢\phi \to F\in \left(X\mathrm{Hom}\left(C\right)Y\right)$$
20	1 16 2 4 6 5	isohom	$$⊢\phi \to YIX\subseteq Y\mathrm{Hom}\left(C\right)X$$
21	1 3 4 5 6 2	invf	$$⊢\phi \to \left(XNY\right):XIY⟶YIX$$
22	21 7	ffvelcdmd	$$⊢\phi \to \left(XNY\right)\left(F\right)\in \left(YIX\right)$$
23	20 22	sseldd	$$⊢\phi \to \left(XNY\right)\left(F\right)\in \left(Y\mathrm{Hom}\left(C\right)X\right)$$
24	1 16 17 8 11 4 5 6 19 23	issect2	$$⊢\phi \to \left(F\left(X\mathrm{Sect}\left(C\right)Y\right)\left(XNY\right)\left(F\right)\leftrightarrow \left(XNY\right)\left(F\right)\left(⟨X,Y⟩\mathrm{comp}\left(C\right)X\right)F=\underset{\dot{}}{1}\left(X\right)\right)$$
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 |-