Theorem isorcl

Description: Reverse closure for isomorphism relations. (Contributed by Zhi Wang, 17-Nov-2025)

	Ref	Expression
Hypotheses	isorcl.i	|- I = ( Iso ` C )
	isorcl.f	|- ( ph -> F e. ( X I Y ) )
Assertion	isorcl	|- ( ph -> C e. Cat )

Proof

Step	Hyp	Ref	Expression
1		isorcl.i	|- I = ( Iso ` C )
2		isorcl.f	|- ( ph -> F e. ( X I Y ) )
3		elfvne0	|- ( F e. ( I ` <. X , Y >. ) -> I =/= (/) )
4		df-ov	|- ( X I Y ) = ( I ` <. X , Y >. )
5	3 4	eleq2s	|- ( F e. ( X I Y ) -> I =/= (/) )
6	1	neeq1i	|- ( I =/= (/) <-> ( Iso ` C ) =/= (/) )
7		n0	|- ( ( Iso ` C ) =/= (/) <-> E. x x e. ( Iso ` C ) )
8	6 7	bitri	|- ( I =/= (/) <-> E. x x e. ( Iso ` C ) )
9	5 8	sylib	|- ( F e. ( X I Y ) -> E. x x e. ( Iso ` C ) )
10		df-iso	|- Iso = ( c e. Cat |-> ( ( x e. _V |-> dom x ) o. ( Inv ` c ) ) )
11	10	mptrcl	|- ( x e. ( Iso ` C ) -> C e. Cat )
12	11	exlimiv	|- ( E. x x e. ( Iso ` C ) -> C e. Cat )
13	2 9 12	3syl	|- ( ph -> C e. Cat )