isoval2

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

Step	Hyp	Ref	Expression
1		isoval2.n	$⊢ N = Inv (C)$
2		isoval2.i	$⊢ I = Iso (C)$
3		id	$⊢ f \in (X I Y) \to f \in (X I Y)$
4		eqid	$⊢ {Base}_{C} = {Base}_{C}$
5	2 3	isorcl	$⊢ f \in (X I Y) \to C \in Cat$
6	2 3 4	isorcl2	$⊢ f \in (X I Y) \to (X \in {Base}_{C} \land Y \in {Base}_{C})$
7	6	simpld	$⊢ f \in (X I Y) \to X \in {Base}_{C}$
8	6	simprd	$⊢ f \in (X I Y) \to Y \in {Base}_{C}$
9	4 1 5 7 8 2	isoval	$⊢ f \in (X I Y) \to X I Y = dom (X N Y)$
10	3 9	eleqtrd	$⊢ f \in (X I Y) \to f \in dom (X N Y)$
11		vex	$⊢ f \in V$
12	11	eldm	$⊢ f \in dom (X N Y) \leftrightarrow \exists g f (X N Y) g$
13		id	$⊢ f (X N Y) g \to f (X N Y) g$
14	1 13	invrcl	$⊢ f (X N Y) g \to C \in Cat$
15	1 13 4	invrcl2	$⊢ f (X N Y) g \to (X \in {Base}_{C} \land Y \in {Base}_{C})$
16	15	simpld	$⊢ f (X N Y) g \to X \in {Base}_{C}$
17	15	simprd	$⊢ f (X N Y) g \to Y \in {Base}_{C}$
18	4 1 14 16 17 2 13	inviso1	$⊢ f (X N Y) g \to f \in (X I Y)$
19	18	exlimiv	$⊢ \exists g f (X N Y) g \to f \in (X I Y)$
20	12 19	sylbi	$⊢ f \in dom (X N Y) \to f \in (X I Y)$
21	10 20	impbii	$⊢ f \in (X I Y) \leftrightarrow f \in dom (X N Y)$
22	21	eqriv	$⊢ X I Y = dom (X N Y)$

Metamath Proof Explorer