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 φ U V
thinccisod.x φ X U
thinccisod.y φ Y U
thinccisod.xt φ X ThinCat
thinccisod.yt φ Y ThinCat
thinccisod.f φ F : R 1-1 onto S
thinccisod.1 φ x R y R x H y = F x J F y =
Assertion thinccisod φ X 𝑐 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 φ U V
7 thinccisod.x φ X U
8 thinccisod.y φ Y U
9 thinccisod.xt φ X ThinCat
10 thinccisod.yt φ Y ThinCat
11 thinccisod.f φ F : R 1-1 onto S
12 thinccisod.1 φ x R y R x H y = F x J F y =
13 f1of F : R 1-1 onto S F : R S
14 11 13 syl φ F : R S
15 fvexd φ Base X V
16 2 15 eqeltrid φ R V
17 14 16 fexd φ F V
18 12 ralrimivva φ x R y R x H y = F x J F y =
19 18 11 jca φ x R y 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 x R y R x H y = f x J f y = x R y 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 x R y R x H y = f x J f y = f : R 1-1 onto S x R y R x H y = F x J F y = F : R 1-1 onto S
28 17 19 27 spcedv φ f x R y R x H y = f x J f y = f : R 1-1 onto S
29 eqid Base C = Base C
30 9 thinccd φ X Cat
31 7 30 elind φ X U Cat
32 1 29 6 catcbas φ Base C = U Cat
33 31 32 eleqtrrd φ X Base C
34 10 thinccd φ Y Cat
35 8 34 elind φ Y U Cat
36 35 32 eleqtrrd φ Y Base C
37 1 29 2 3 4 5 6 33 36 9 10 thincciso φ X 𝑐 C Y f x R y R x H y = f x J f y = f : R 1-1 onto S
38 28 37 mpbird φ X 𝑐 C Y