Theorem isocoinvid

Description: The inverse of an isomorphism composed with the isomorphism is the identity. (Contributed by AV, 10-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)$$
	isocoinvid.o	No typesetting found for |- .o. = ( <. Y , X >. ( comp ` C ) Y ) with typecode |-
Assertion	isocoinvid	Could not format assertion : No typesetting found for |- ( ph -> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) ) 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		isocoinvid.o	Could not format .o. = ( <. Y , X >. ( comp ` C ) Y ) : No typesetting found for |- .o. = ( <. Y , X >. ( comp ` C ) Y ) with typecode |-
10	1 2 3 4 5 6 7	invisoinvl	$$⊢\phi \to \left(XNY\right)\left(F\right)\left(YNX\right)F$$
11		eqid	$$⊢\mathrm{Sect}\left(C\right)=\mathrm{Sect}\left(C\right)$$
12	1 3 4 6 5 11	isinv	$$⊢\phi \to \left(\left(XNY\right)\left(F\right)\left(YNX\right)F\leftrightarrow \left(\left(XNY\right)\left(F\right)\left(Y\mathrm{Sect}\left(C\right)X\right)F\wedge F\left(X\mathrm{Sect}\left(C\right)Y\right)\left(XNY\right)\left(F\right)\right)\right)$$
13		simpl	$$⊢\left(\left(XNY\right)\left(F\right)\left(Y\mathrm{Sect}\left(C\right)X\right)F\wedge F\left(X\mathrm{Sect}\left(C\right)Y\right)\left(XNY\right)\left(F\right)\right)\to \left(XNY\right)\left(F\right)\left(Y\mathrm{Sect}\left(C\right)X\right)F$$
14	12 13	biimtrdi	$$⊢\phi \to \left(\left(XNY\right)\left(F\right)\left(YNX\right)F\to \left(XNY\right)\left(F\right)\left(Y\mathrm{Sect}\left(C\right)X\right)F\right)$$
15	10 14	mpd	$$⊢\phi \to \left(XNY\right)\left(F\right)\left(Y\mathrm{Sect}\left(C\right)X\right)F$$
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 6 5	isohom	$$⊢\phi \to YIX\subseteq Y\mathrm{Hom}\left(C\right)X$$
19	1 3 4 5 6 2	invf	$$⊢\phi \to \left(XNY\right):XIY⟶YIX$$
20	19 7	ffvelcdmd	$$⊢\phi \to \left(XNY\right)\left(F\right)\in \left(YIX\right)$$
21	18 20	sseldd	$$⊢\phi \to \left(XNY\right)\left(F\right)\in \left(Y\mathrm{Hom}\left(C\right)X\right)$$
22	1 16 2 4 5 6	isohom	$$⊢\phi \to XIY\subseteq X\mathrm{Hom}\left(C\right)Y$$
23	22 7	sseldd	$$⊢\phi \to F\in \left(X\mathrm{Hom}\left(C\right)Y\right)$$
24	1 16 17 8 11 4 6 5 21 23	issect2	$$⊢\phi \to \left(\left(XNY\right)\left(F\right)\left(Y\mathrm{Sect}\left(C\right)X\right)F\leftrightarrow F\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)\left(XNY\right)\left(F\right)=\underset{\dot{}}{1}\left(Y\right)\right)$$
25	9	a1i	Could not format ( ph -> .o. = ( <. Y , X >. ( comp ` C ) Y ) ) : No typesetting found for |- ( ph -> .o. = ( <. Y , X >. ( comp ` C ) Y ) ) with typecode |-
26	25	eqcomd	Could not format ( ph -> ( <. Y , X >. ( comp ` C ) Y ) = .o. ) : No typesetting found for |- ( ph -> ( <. Y , X >. ( comp ` C ) Y ) = .o. ) with typecode |-
27	26	oveqd	Could not format ( ph -> ( F ( <. Y , X >. ( comp ` C ) Y ) ( ( X N Y ) ` F ) ) = ( F .o. ( ( X N Y ) ` F ) ) ) : No typesetting found for |- ( ph -> ( F ( <. Y , X >. ( comp ` C ) Y ) ( ( X N Y ) ` F ) ) = ( F .o. ( ( X N Y ) ` F ) ) ) with typecode |-
28	27	eqeq1d	Could not format ( ph -> ( ( F ( <. Y , X >. ( comp ` C ) Y ) ( ( X N Y ) ` F ) ) = ( .1. ` Y ) <-> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) ) ) : No typesetting found for |- ( ph -> ( ( F ( <. Y , X >. ( comp ` C ) Y ) ( ( X N Y ) ` F ) ) = ( .1. ` Y ) <-> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) ) ) with typecode |-
29	24 28	bitrd	Could not format ( ph -> ( ( ( X N Y ) ` F ) ( Y ( Sect ` C ) X ) F <-> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) ) ) : No typesetting found for |- ( ph -> ( ( ( X N Y ) ` F ) ( Y ( Sect ` C ) X ) F <-> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) ) ) with typecode |-
30	15 29	mpbid	Could not format ( ph -> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) ) : No typesetting found for |- ( ph -> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) ) with typecode |-