Metamath Proof Explorer


Theorem oduoppcciso

Description: The dual of a preordered set and the opposite category are category-isomorphic. Example 3.6(1) of Adamek p. 25. (Contributed by Zhi Wang, 22-Sep-2025)

Ref Expression
Hypotheses prstcnid.c φ C = ProsetToCat K
prstcnid.k φ K Proset
oduoppcbas.d φ D = ProsetToCat ODual K
oduoppcbas.o O = oppCat C
oduoppcciso.u φ U V
oduoppcciso.d φ D U
oduoppcciso.o φ O U
Assertion oduoppcciso φ D 𝑐 CatCat U O

Proof

Step Hyp Ref Expression
1 prstcnid.c φ C = ProsetToCat K
2 prstcnid.k φ K Proset
3 oduoppcbas.d φ D = ProsetToCat ODual K
4 oduoppcbas.o O = oppCat C
5 oduoppcciso.u φ U V
6 oduoppcciso.d φ D U
7 oduoppcciso.o φ O U
8 eqid CatCat U = CatCat U
9 eqid Base D = Base D
10 eqid Base O = Base O
11 eqid Hom D = Hom D
12 eqid Hom O = Hom O
13 eqid ODual K = ODual K
14 13 oduprs K Proset ODual K Proset
15 2 14 syl φ ODual K Proset
16 3 15 prstcthin φ D ThinCat
17 1 2 prstcthin φ C ThinCat
18 4 oppcthin C ThinCat O ThinCat
19 17 18 syl φ O ThinCat
20 f1oi I Base D : Base D 1-1 onto Base D
21 1 2 3 4 oduoppcbas φ Base D = Base O
22 21 f1oeq3d φ I Base D : Base D 1-1 onto Base D I Base D : Base D 1-1 onto Base O
23 20 22 mpbii φ I Base D : Base D 1-1 onto Base O
24 eqid K = K
25 eqid ODual K = ODual K
26 13 24 25 oduleg x Base D y Base D x ODual K y y K x
27 26 adantl φ x Base D y Base D x ODual K y y K x
28 3 adantr φ x Base D y Base D D = ProsetToCat ODual K
29 2 adantr φ x Base D y Base D K Proset
30 29 14 syl φ x Base D y Base D ODual K Proset
31 eqidd φ x Base D y Base D ODual K = ODual K
32 28 30 31 prstcleval φ x Base D y Base D ODual K = D
33 eqidd φ x Base D y Base D Hom D = Hom D
34 simprl φ x Base D y Base D x Base D
35 simprr φ x Base D y Base D y Base D
36 28 30 32 33 34 35 prstchom φ x Base D y Base D x ODual K y x Hom D y
37 1 adantr φ x Base D y Base D C = ProsetToCat K
38 eqidd φ x Base D y Base D K = K
39 37 29 38 prstcleval φ x Base D y Base D K = C
40 eqidd φ x Base D y Base D Hom C = Hom C
41 eqid Base C = Base C
42 4 41 oppcbas Base C = Base O
43 21 42 eqtr4di φ Base D = Base C
44 43 adantr φ x Base D y Base D Base D = Base C
45 35 44 eleqtrd φ x Base D y Base D y Base C
46 34 44 eleqtrd φ x Base D y Base D x Base C
47 37 29 39 40 45 46 prstchom φ x Base D y Base D y K x y Hom C x
48 27 36 47 3bitr3d φ x Base D y Base D x Hom D y y Hom C x
49 48 necon4bid φ x Base D y Base D x Hom D y = y Hom C x =
50 fvresi x Base D I Base D x = x
51 50 ad2antrl φ x Base D y Base D I Base D x = x
52 fvresi y Base D I Base D y = y
53 52 ad2antll φ x Base D y Base D I Base D y = y
54 51 53 oveq12d φ x Base D y Base D I Base D x Hom O I Base D y = x Hom O y
55 eqid Hom C = Hom C
56 55 4 oppchom x Hom O y = y Hom C x
57 54 56 eqtrdi φ x Base D y Base D I Base D x Hom O I Base D y = y Hom C x
58 57 eqeq1d φ x Base D y Base D I Base D x Hom O I Base D y = y Hom C x =
59 49 58 bitr4d φ x Base D y Base D x Hom D y = I Base D x Hom O I Base D y =
60 8 9 10 11 12 5 6 7 16 19 23 59 thinccisod φ D 𝑐 CatCat U O