Metamath Proof Explorer

Theorem thinccisod

Description: Two thin categories are isomorphic if the induced preorders are order-isomorphic (deduction form). Example 3.26(2) of Adamek p. 33. (Contributed by Zhi Wang, 22-Sep-2025)

Ref Expression
Hypotheses thinccisod.c 
|- C = ( CatCat ` U )
thinccisod.r 
|- R = ( Base ` X )
thinccisod.s 
|- S = ( Base ` Y )
thinccisod.h 
|- H = ( Hom ` X )
thinccisod.j 
|- J = ( Hom ` Y )
thinccisod.u 
|- ( ph -> U e. V )
thinccisod.x 
|- ( ph -> X e. U )
thinccisod.y 
|- ( ph -> Y e. U )
thinccisod.xt 
|- ( ph -> X e. ThinCat )
thinccisod.yt 
|- ( ph -> Y e. ThinCat )
thinccisod.f 
|- ( ph -> F : R -1-1-onto-> S )
thinccisod.1 
|- ( ( ph /\ ( x e. R /\ y e. R ) ) -> ( ( x H y ) = (/) <-> ( ( F ` x ) J ( F ` y ) ) = (/) ) )
Assertion thinccisod 
|- ( ph -> X ( ~=c ` C ) Y )

Proof

Step Hyp Ref Expression
1 thinccisod.c 
 |-  C = ( CatCat ` U )
2 thinccisod.r 
 |-  R = ( Base ` X )
3 thinccisod.s 
 |-  S = ( Base ` Y )
4 thinccisod.h 
 |-  H = ( Hom ` X )
5 thinccisod.j 
 |-  J = ( Hom ` Y )
6 thinccisod.u 
 |-  ( ph -> U e. V )
7 thinccisod.x 
 |-  ( ph -> X e. U )
8 thinccisod.y 
 |-  ( ph -> Y e. U )
9 thinccisod.xt 
 |-  ( ph -> X e. ThinCat )
10 thinccisod.yt 
 |-  ( ph -> Y e. ThinCat )
11 thinccisod.f 
 |-  ( ph -> F : R -1-1-onto-> S )
12 thinccisod.1 
 |-  ( ( ph /\ ( x e. R /\ y e. R ) ) -> ( ( x H y ) = (/) <-> ( ( F ` x ) J ( F ` y ) ) = (/) ) )
13 f1of 
 |-  ( F : R -1-1-onto-> S -> F : R --> S )
14 11 13 syl 
 |-  ( ph -> F : R --> S )
15 fvexd 
 |-  ( ph -> ( Base ` X ) e. _V )
16 2 15 eqeltrid 
 |-  ( ph -> R e. _V )
17 14 16 fexd 
 |-  ( ph -> F e. _V )
18 12 ralrimivva 
 |-  ( ph -> A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( F ` x ) J ( F ` y ) ) = (/) ) )
19 18 11 jca 
 |-  ( ph -> ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( F ` x ) J ( F ` y ) ) = (/) ) /\ F : R -1-1-onto-> S ) )
20 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
21 fveq1 
 |-  ( f = F -> ( f ` y ) = ( F ` y ) )
22 20 21 oveq12d 
 |-  ( f = F -> ( ( f ` x ) J ( f ` y ) ) = ( ( F ` x ) J ( F ` y ) ) )
23 22 eqeq1d 
 |-  ( f = F -> ( ( ( f ` x ) J ( f ` y ) ) = (/) <-> ( ( F ` x ) J ( F ` y ) ) = (/) ) )
24 23 bibi2d 
 |-  ( f = F -> ( ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) <-> ( ( x H y ) = (/) <-> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) )
25 24 2ralbidv 
 |-  ( f = F -> ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) <-> A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) )
26 f1oeq1 
 |-  ( f = F -> ( f : R -1-1-onto-> S <-> F : R -1-1-onto-> S ) )
27 25 26 anbi12d 
 |-  ( f = F -> ( ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) <-> ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( F ` x ) J ( F ` y ) ) = (/) ) /\ F : R -1-1-onto-> S ) ) )
28 17 19 27 spcedv 
 |-  ( ph -> E. f ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) )
29 eqid 
 |-  ( Base ` C ) = ( Base ` C )
30 9 thinccd 
 |-  ( ph -> X e. Cat )
31 7 30 elind 
 |-  ( ph -> X e. ( U i^i Cat ) )
32 1 29 6 catcbas 
 |-  ( ph -> ( Base ` C ) = ( U i^i Cat ) )
33 31 32 eleqtrrd 
 |-  ( ph -> X e. ( Base ` C ) )
34 10 thinccd 
 |-  ( ph -> Y e. Cat )
35 8 34 elind 
 |-  ( ph -> Y e. ( U i^i Cat ) )
36 35 32 eleqtrrd 
 |-  ( ph -> Y e. ( Base ` C ) )
37 1 29 2 3 4 5 6 33 36 9 10 thincciso 
 |-  ( ph -> ( X ( ~=c ` C ) Y <-> E. f ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) )
38 28 37 mpbird 
 |-  ( ph -> X ( ~=c ` C ) Y )