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

Metamath Proof Explorer

Theorem catcrcl

Description: Reverse closure for the category of categories (in a universe) (Contributed by Zhi Wang, 14-Nov-2025)

Ref Expression
Hypotheses catcrcl.c 
|- C = ( CatCat ` U )
catcrcl.h 
|- H = ( Hom ` C )
catcrcl.f 
|- ( ph -> F e. ( X H Y ) )
Assertion catcrcl 
|- ( ph -> U e. _V )

Proof

Step Hyp Ref Expression
1 catcrcl.c 
 |-  C = ( CatCat ` U )
2 catcrcl.h 
 |-  H = ( Hom ` C )
3 catcrcl.f 
 |-  ( ph -> F e. ( X H Y ) )
4 elfvne0 
 |-  ( F e. ( H ` <. X , Y >. ) -> H =/= (/) )
5 df-ov 
 |-  ( X H Y ) = ( H ` <. X , Y >. )
6 4 5 eleq2s 
 |-  ( F e. ( X H Y ) -> H =/= (/) )
7 fvprc 
 |-  ( -. U e. _V -> ( CatCat ` U ) = (/) )
8 1 7 eqtrid 
 |-  ( -. U e. _V -> C = (/) )
9 fveq2 
 |-  ( C = (/) -> ( Hom ` C ) = ( Hom ` (/) ) )
10 homid 
 |-  Hom = Slot ( Hom ` ndx )
11 10 str0 
 |-  (/) = ( Hom ` (/) )
12 9 2 11 3eqtr4g 
 |-  ( C = (/) -> H = (/) )
13 8 12 syl 
 |-  ( -. U e. _V -> H = (/) )
14 13 necon1ai 
 |-  ( H =/= (/) -> U e. _V )
15 3 6 14 3syl 
 |-  ( ph -> U e. _V )