Theorem isoval2

Description: The isomorphisms are the domain of the inverse relation. (Contributed by Zhi Wang, 17-Nov-2025)

	Ref	Expression
Hypotheses	isoval2.n	|- N = ( Inv ` C )
	isoval2.i	|- I = ( Iso ` C )
Assertion	isoval2	|- ( X I Y ) = dom ( X N Y )

Proof

Step	Hyp	Ref	Expression
1		isoval2.n	|- N = ( Inv ` C )
2		isoval2.i	|- I = ( Iso ` C )
3		id	|- ( f e. ( X I Y ) -> f e. ( X I Y ) )
4		eqid	|- ( Base ` C ) = ( Base ` C )
5	2 3	isorcl	|- ( f e. ( X I Y ) -> C e. Cat )
6	2 3 4	isorcl2	|- ( f e. ( X I Y ) -> ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) )
7	6	simpld	|- ( f e. ( X I Y ) -> X e. ( Base ` C ) )
8	6	simprd	|- ( f e. ( X I Y ) -> Y e. ( Base ` C ) )
9	4 1 5 7 8 2	isoval	|- ( f e. ( X I Y ) -> ( X I Y ) = dom ( X N Y ) )
10	3 9	eleqtrd	|- ( f e. ( X I Y ) -> f e. dom ( X N Y ) )
11		vex	|- f e. _V
12	11	eldm	|- ( f e. dom ( X N Y ) <-> E. g f ( X N Y ) g )
13		id	|- ( f ( X N Y ) g -> f ( X N Y ) g )
14	1 13	invrcl	|- ( f ( X N Y ) g -> C e. Cat )
15	1 13 4	invrcl2	|- ( f ( X N Y ) g -> ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) )
16	15	simpld	|- ( f ( X N Y ) g -> X e. ( Base ` C ) )
17	15	simprd	|- ( f ( X N Y ) g -> Y e. ( Base ` C ) )
18	4 1 14 16 17 2 13	inviso1	|- ( f ( X N Y ) g -> f e. ( X I Y ) )
19	18	exlimiv	|- ( E. g f ( X N Y ) g -> f e. ( X I Y ) )
20	12 19	sylbi	|- ( f e. dom ( X N Y ) -> f e. ( X I Y ) )
21	10 20	impbii	|- ( f e. ( X I Y ) <-> f e. dom ( X N Y ) )
22	21	eqriv	|- ( X I Y ) = dom ( X N Y )