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

Metamath Proof Explorer

Theorem isorcl

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 ) )
Assertion isorcl 
|- ( ph -> C e. Cat )

Proof

Step Hyp Ref Expression
1 isorcl.i 
 |-  I = ( Iso ` C )
2 isorcl.f 
 |-  ( ph -> F e. ( X I Y ) )
3 elfvne0 
 |-  ( F e. ( I ` <. X , Y >. ) -> I =/= (/) )
4 df-ov 
 |-  ( X I Y ) = ( I ` <. X , Y >. )
5 3 4 eleq2s 
 |-  ( F e. ( X I Y ) -> I =/= (/) )
6 1 neeq1i 
 |-  ( I =/= (/) <-> ( Iso ` C ) =/= (/) )
7 n0 
 |-  ( ( Iso ` C ) =/= (/) <-> E. x x e. ( Iso ` C ) )
8 6 7 bitri 
 |-  ( I =/= (/) <-> E. x x e. ( Iso ` C ) )
9 5 8 sylib 
 |-  ( F e. ( X I Y ) -> E. x x e. ( Iso ` C ) )
10 df-iso 
 |-  Iso = ( c e. Cat |-> ( ( x e. _V |-> dom x ) o. ( Inv ` c ) ) )
11 10 mptrcl 
 |-  ( x e. ( Iso ` C ) -> C e. Cat )
12 11 exlimiv 
 |-  ( E. x x e. ( Iso ` C ) -> C e. Cat )
13 2 9 12 3syl 
 |-  ( ph -> C e. Cat )