Theorem isoval2

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

	Ref	Expression
Hypotheses	isoval2.n	⊢ 𝑁 = ( Inv ‘ 𝐶 )
	isoval2.i	⊢ 𝐼 = ( Iso ‘ 𝐶 )
Assertion	isoval2	⊢ ( 𝑋 𝐼 𝑌 ) = dom ( 𝑋 𝑁 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		isoval2.n	⊢ 𝑁 = ( Inv ‘ 𝐶 )
2		isoval2.i	⊢ 𝐼 = ( Iso ‘ 𝐶 )
3		id	⊢ ( 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) → 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) )
4		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5	2 3	isorcl	⊢ ( 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) → 𝐶 ∈ Cat )
6	2 3 4	isorcl2	⊢ ( 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) → ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
7	6	simpld	⊢ ( 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) → 𝑋 ∈ ( Base ‘ 𝐶 ) )
8	6	simprd	⊢ ( 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) → 𝑌 ∈ ( Base ‘ 𝐶 ) )
9	4 1 5 7 8 2	isoval	⊢ ( 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) → ( 𝑋 𝐼 𝑌 ) = dom ( 𝑋 𝑁 𝑌 ) )
10	3 9	eleqtrd	⊢ ( 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) → 𝑓 ∈ dom ( 𝑋 𝑁 𝑌 ) )
11		vex	⊢ 𝑓 ∈ V
12	11	eldm	⊢ ( 𝑓 ∈ dom ( 𝑋 𝑁 𝑌 ) ↔ ∃ 𝑔 𝑓 ( 𝑋 𝑁 𝑌 ) 𝑔 )
13		id	⊢ ( 𝑓 ( 𝑋 𝑁 𝑌 ) 𝑔 → 𝑓 ( 𝑋 𝑁 𝑌 ) 𝑔 )
14	1 13	invrcl	⊢ ( 𝑓 ( 𝑋 𝑁 𝑌 ) 𝑔 → 𝐶 ∈ Cat )
15	1 13 4	invrcl2	⊢ ( 𝑓 ( 𝑋 𝑁 𝑌 ) 𝑔 → ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
16	15	simpld	⊢ ( 𝑓 ( 𝑋 𝑁 𝑌 ) 𝑔 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
17	15	simprd	⊢ ( 𝑓 ( 𝑋 𝑁 𝑌 ) 𝑔 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
18	4 1 14 16 17 2 13	inviso1	⊢ ( 𝑓 ( 𝑋 𝑁 𝑌 ) 𝑔 → 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) )
19	18	exlimiv	⊢ ( ∃ 𝑔 𝑓 ( 𝑋 𝑁 𝑌 ) 𝑔 → 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) )
20	12 19	sylbi	⊢ ( 𝑓 ∈ dom ( 𝑋 𝑁 𝑌 ) → 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) )
21	10 20	impbii	⊢ ( 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) ↔ 𝑓 ∈ dom ( 𝑋 𝑁 𝑌 ) )
22	21	eqriv	⊢ ( 𝑋 𝐼 𝑌 ) = dom ( 𝑋 𝑁 𝑌 )