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

Metamath Proof Explorer

Theorem isorcl2

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 ) )
isorcl2.b 
|- B = ( Base ` C )
Assertion isorcl2 
|- ( ph -> ( X e. B /\ Y e. B ) )

Proof

Step Hyp Ref Expression
1 isorcl.i 
 |-  I = ( Iso ` C )
2 isorcl.f 
 |-  ( ph -> F e. ( X I Y ) )
3 isorcl2.b 
 |-  B = ( Base ` C )
4 eqid 
 |-  ( Inv ` C ) = ( Inv ` C )
5 1 2 isorcl 
 |-  ( ph -> C e. Cat )
6 3 4 5 1 isofval2 
 |-  ( ph -> I = ( x e. B , y e. B |-> dom ( x ( Inv ` C ) y ) ) )
7 6 oveqd 
 |-  ( ph -> ( X I Y ) = ( X ( x e. B , y e. B |-> dom ( x ( Inv ` C ) y ) ) Y ) )
8 2 7 eleqtrd 
 |-  ( ph -> F e. ( X ( x e. B , y e. B |-> dom ( x ( Inv ` C ) y ) ) Y ) )
9 eqid 
 |-  ( x e. B , y e. B |-> dom ( x ( Inv ` C ) y ) ) = ( x e. B , y e. B |-> dom ( x ( Inv ` C ) y ) )
10 9 elmpocl 
 |-  ( F e. ( X ( x e. B , y e. B |-> dom ( x ( Inv ` C ) y ) ) Y ) -> ( X e. B /\ Y e. B ) )
11 8 10 syl 
 |-  ( ph -> ( X e. B /\ Y e. B ) )