This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )