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

Metamath Proof Explorer

Theorem catcrcl2

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

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 catcrcl2.b 
 |-  B = ( Base ` C )
5 1 2 3 catcrcl 
 |-  ( ph -> U e. _V )
6 1 4 5 2 catchomfval 
 |-  ( ph -> H = ( x e. B , y e. B |-> ( x Func y ) ) )
7 6 oveqd 
 |-  ( ph -> ( X H Y ) = ( X ( x e. B , y e. B |-> ( x Func y ) ) Y ) )
8 3 7 eleqtrd 
 |-  ( ph -> F e. ( X ( x e. B , y e. B |-> ( x Func y ) ) Y ) )
9 eqid 
 |-  ( x e. B , y e. B |-> ( x Func y ) ) = ( x e. B , y e. B |-> ( x Func y ) )
10 9 elmpocl 
 |-  ( F e. ( X ( x e. B , y e. B |-> ( x Func y ) ) Y ) -> ( X e. B /\ Y e. B ) )
11 8 10 syl 
 |-  ( ph -> ( X e. B /\ Y e. B ) )