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

Metamath Proof Explorer

Theorem isthincd

Description: The predicate "is a thin category" (deduction form). (Contributed by Zhi Wang, 17-Sep-2024)

Ref Expression
Hypotheses isthincd.b 
|- ( ph -> B = ( Base ` C ) )
isthincd.h 
|- ( ph -> H = ( Hom ` C ) )
isthincd.t 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> E* f f e. ( x H y ) )
isthincd.c 
|- ( ph -> C e. Cat )
Assertion isthincd 
|- ( ph -> C e. ThinCat )

Proof

Step Hyp Ref Expression
1 isthincd.b 
 |-  ( ph -> B = ( Base ` C ) )
2 isthincd.h 
 |-  ( ph -> H = ( Hom ` C ) )
3 isthincd.t 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> E* f f e. ( x H y ) )
4 isthincd.c 
 |-  ( ph -> C e. Cat )
5 3 ralrimivva 
 |-  ( ph -> A. x e. B A. y e. B E* f f e. ( x H y ) )
6 2 oveqd 
 |-  ( ph -> ( x H y ) = ( x ( Hom ` C ) y ) )
7 6 eleq2d 
 |-  ( ph -> ( f e. ( x H y ) <-> f e. ( x ( Hom ` C ) y ) ) )
8 7 mobidv 
 |-  ( ph -> ( E* f f e. ( x H y ) <-> E* f f e. ( x ( Hom ` C ) y ) ) )
9 1 8 raleqbidv 
 |-  ( ph -> ( A. y e. B E* f f e. ( x H y ) <-> A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` C ) y ) ) )
10 1 9 raleqbidv 
 |-  ( ph -> ( A. x e. B A. y e. B E* f f e. ( x H y ) <-> A. x e. ( Base ` C ) A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` C ) y ) ) )
11 5 10 mpbid 
 |-  ( ph -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` C ) y ) )
12 eqid 
 |-  ( Base ` C ) = ( Base ` C )
13 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
14 12 13 isthinc 
 |-  ( C e. ThinCat <-> ( C e. Cat /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` C ) y ) ) )
15 4 11 14 sylanbrc 
 |-  ( ph -> C e. ThinCat )