Theorem isisod

Description: The predicate "is an isomorphism" (deduction form). (Contributed by Zhi Wang, 16-Sep-2025)

	Ref	Expression
Hypotheses	isisod.b	$$⊢B={\mathrm{Base}}_C$$
	isisod.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	isisod.o	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
	isisod.i	$$⊢I=\mathrm{Iso}\left(C\right)$$
	isisod.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
	isisod.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	isisod.x	$$⊢\phi \to X\in B$$
	isisod.y	$$⊢\phi \to Y\in B$$
	isisod.f	$$⊢\phi \to F\in \left(XHY\right)$$
	isisod.g	$$⊢\phi \to G\in \left(YHX\right)$$
	isisod.gf	$$⊢\phi \to G\left(⟨X,Y⟩\underset{\dot{}}{·}X\right)F=\underset{\dot{}}{1}\left(X\right)$$
	isisod.fg	$$⊢\phi \to F\left(⟨Y,X⟩\underset{\dot{}}{·}Y\right)G=\underset{\dot{}}{1}\left(Y\right)$$
Assertion	isisod	$$⊢\phi \to F\in \left(XIY\right)$$

Proof

Step	Hyp	Ref	Expression
1		isisod.b	$$⊢B={\mathrm{Base}}_C$$
2		isisod.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
3		isisod.o	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
4		isisod.i	$$⊢I=\mathrm{Iso}\left(C\right)$$
5		isisod.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
6		isisod.c	$$⊢\phi \to C\in \mathrm{Cat}$$
7		isisod.x	$$⊢\phi \to X\in B$$
8		isisod.y	$$⊢\phi \to Y\in B$$
9		isisod.f	$$⊢\phi \to F\in \left(XHY\right)$$
10		isisod.g	$$⊢\phi \to G\in \left(YHX\right)$$
11		isisod.gf	$$⊢\phi \to G\left(⟨X,Y⟩\underset{\dot{}}{·}X\right)F=\underset{\dot{}}{1}\left(X\right)$$
12		isisod.fg	$$⊢\phi \to F\left(⟨Y,X⟩\underset{\dot{}}{·}Y\right)G=\underset{\dot{}}{1}\left(Y\right)$$
13		simpr	$$⊢\left(\phi \wedge g=G\right)\to g=G$$
14	13	oveq1d	$$⊢\left(\phi \wedge g=G\right)\to g\left(⟨X,Y⟩\underset{\dot{}}{·}X\right)F=G\left(⟨X,Y⟩\underset{\dot{}}{·}X\right)F$$
15	14	eqeq1d	$$⊢\left(\phi \wedge g=G\right)\to \left(g\left(⟨X,Y⟩\underset{\dot{}}{·}X\right)F=\underset{\dot{}}{1}\left(X\right)\leftrightarrow G\left(⟨X,Y⟩\underset{\dot{}}{·}X\right)F=\underset{\dot{}}{1}\left(X\right)\right)$$
16	13	oveq2d	$$⊢\left(\phi \wedge g=G\right)\to F\left(⟨Y,X⟩\underset{\dot{}}{·}Y\right)g=F\left(⟨Y,X⟩\underset{\dot{}}{·}Y\right)G$$
17	16	eqeq1d	$$⊢\left(\phi \wedge g=G\right)\to \left(F\left(⟨Y,X⟩\underset{\dot{}}{·}Y\right)g=\underset{\dot{}}{1}\left(Y\right)\leftrightarrow F\left(⟨Y,X⟩\underset{\dot{}}{·}Y\right)G=\underset{\dot{}}{1}\left(Y\right)\right)$$
18	15 17	anbi12d	$$⊢\left(\phi \wedge g=G\right)\to \left(\left(g\left(⟨X,Y⟩\underset{\dot{}}{·}X\right)F=\underset{\dot{}}{1}\left(X\right)\wedge F\left(⟨Y,X⟩\underset{\dot{}}{·}Y\right)g=\underset{\dot{}}{1}\left(Y\right)\right)\leftrightarrow \left(G\left(⟨X,Y⟩\underset{\dot{}}{·}X\right)F=\underset{\dot{}}{1}\left(X\right)\wedge F\left(⟨Y,X⟩\underset{\dot{}}{·}Y\right)G=\underset{\dot{}}{1}\left(Y\right)\right)\right)$$
19	10 18	rspcedv	$$⊢\phi \to \left(\left(G\left(⟨X,Y⟩\underset{\dot{}}{·}X\right)F=\underset{\dot{}}{1}\left(X\right)\wedge F\left(⟨Y,X⟩\underset{\dot{}}{·}Y\right)G=\underset{\dot{}}{1}\left(Y\right)\right)\to \exists g\in \left(YHX\right)\left(g\left(⟨X,Y⟩\underset{\dot{}}{·}X\right)F=\underset{\dot{}}{1}\left(X\right)\wedge F\left(⟨Y,X⟩\underset{\dot{}}{·}Y\right)g=\underset{\dot{}}{1}\left(Y\right)\right)\right)$$
20	11 12 19	mp2and	$$⊢\phi \to \exists g\in \left(YHX\right)\left(g\left(⟨X,Y⟩\underset{\dot{}}{·}X\right)F=\underset{\dot{}}{1}\left(X\right)\wedge F\left(⟨Y,X⟩\underset{\dot{}}{·}Y\right)g=\underset{\dot{}}{1}\left(Y\right)\right)$$
21	3	oveqi	$$⊢⟨X,Y⟩\underset{\dot{}}{·}X=⟨X,Y⟩\mathrm{comp}\left(C\right)X$$
22	3	oveqi	$$⊢⟨Y,X⟩\underset{\dot{}}{·}Y=⟨Y,X⟩\mathrm{comp}\left(C\right)Y$$
23	1 2 6 4 7 8 9 5 21 22	dfiso2	$$⊢\phi \to \left(F\in \left(XIY\right)\leftrightarrow \exists g\in \left(YHX\right)\left(g\left(⟨X,Y⟩\underset{\dot{}}{·}X\right)F=\underset{\dot{}}{1}\left(X\right)\wedge F\left(⟨Y,X⟩\underset{\dot{}}{·}Y\right)g=\underset{\dot{}}{1}\left(Y\right)\right)\right)$$
24	20 23	mpbird	$$⊢\phi \to F\in \left(XIY\right)$$