Metamath Proof Explorer

Theorem thincpropd

Description: Two structures with the same base, hom-sets and composition operation are either both thin categories or neither. (Contributed by Zhi Wang, 16-Oct-2025)

Ref Expression
Hypotheses thincpropd.1 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
thincpropd.2 
|- ( ph -> ( comf ` C ) = ( comf ` D ) )
thincpropd.3 
|- ( ph -> C e. V )
thincpropd.4 
|- ( ph -> D e. W )
Assertion thincpropd 
|- ( ph -> ( C e. ThinCat <-> D e. ThinCat ) )

Proof

Step Hyp Ref Expression
1 thincpropd.1 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
2 thincpropd.2 
 |-  ( ph -> ( comf ` C ) = ( comf ` D ) )
3 thincpropd.3 
 |-  ( ph -> C e. V )
4 thincpropd.4 
 |-  ( ph -> D e. W )
5 1 2 3 4 catpropd 
 |-  ( ph -> ( C e. Cat <-> D e. Cat ) )
6 eqid 
 |-  ( Base ` C ) = ( Base ` C )
7 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
8 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
9 1 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( Homf ` C ) = ( Homf ` D ) )
10 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> x e. ( Base ` C ) )
11 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> y e. ( Base ` C ) )
12 6 7 8 9 10 11 homfeqval 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( Hom ` C ) y ) = ( x ( Hom ` D ) y ) )
13 12 eleq2d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( f e. ( x ( Hom ` C ) y ) <-> f e. ( x ( Hom ` D ) y ) ) )
14 13 mobidv 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( E* f f e. ( x ( Hom ` C ) y ) <-> E* f f e. ( x ( Hom ` D ) y ) ) )
15 14 2ralbidva 
 |-  ( ph -> ( A. x e. ( Base ` C ) A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` C ) y ) <-> A. x e. ( Base ` C ) A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` D ) y ) ) )
16 1 homfeqbas 
 |-  ( ph -> ( Base ` C ) = ( Base ` D ) )
17 16 raleqdv 
 |-  ( ph -> ( A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` D ) y ) <-> A. y e. ( Base ` D ) E* f f e. ( x ( Hom ` D ) y ) ) )
18 16 17 raleqbidv 
 |-  ( ph -> ( A. x e. ( Base ` C ) A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` D ) y ) <-> A. x e. ( Base ` D ) A. y e. ( Base ` D ) E* f f e. ( x ( Hom ` D ) y ) ) )
19 15 18 bitrd 
 |-  ( ph -> ( A. x e. ( Base ` C ) A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` C ) y ) <-> A. x e. ( Base ` D ) A. y e. ( Base ` D ) E* f f e. ( x ( Hom ` D ) y ) ) )
20 5 19 anbi12d 
 |-  ( ph -> ( ( C e. Cat /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` C ) y ) ) <-> ( D e. Cat /\ A. x e. ( Base ` D ) A. y e. ( Base ` D ) E* f f e. ( x ( Hom ` D ) y ) ) ) )
21 6 7 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 ) ) )
22 eqid 
 |-  ( Base ` D ) = ( Base ` D )
23 22 8 isthinc 
 |-  ( D e. ThinCat <-> ( D e. Cat /\ A. x e. ( Base ` D ) A. y e. ( Base ` D ) E* f f e. ( x ( Hom ` D ) y ) ) )
24 20 21 23 3bitr4g 
 |-  ( ph -> ( C e. ThinCat <-> D e. ThinCat ) )