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 
|- ( ph -> C = ( ProsetToCat ` K ) )
prstcnid.k 
|- ( ph -> K e. Proset )
oduoppcbas.d 
|- ( ph -> D = ( ProsetToCat ` ( ODual ` K ) ) )
oduoppcbas.o 
|- O = ( oppCat ` C )
oduoppcciso.u 
|- ( ph -> U e. V )
oduoppcciso.d 
|- ( ph -> D e. U )
oduoppcciso.o 
|- ( ph -> O e. U )
Assertion oduoppcciso 
|- ( ph -> D ( ~=c ` ( CatCat ` U ) ) O )

Proof

Step Hyp Ref Expression
1 prstcnid.c 
 |-  ( ph -> C = ( ProsetToCat ` K ) )
2 prstcnid.k 
 |-  ( ph -> K e. Proset )
3 oduoppcbas.d 
 |-  ( ph -> D = ( ProsetToCat ` ( ODual ` K ) ) )
4 oduoppcbas.o 
 |-  O = ( oppCat ` C )
5 oduoppcciso.u 
 |-  ( ph -> U e. V )
6 oduoppcciso.d 
 |-  ( ph -> D e. U )
7 oduoppcciso.o 
 |-  ( ph -> O e. 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 e. Proset -> ( ODual ` K ) e. Proset )
15 2 14 syl 
 |-  ( ph -> ( ODual ` K ) e. Proset )
16 3 15 prstcthin 
 |-  ( ph -> D e. ThinCat )
17 1 2 prstcthin 
 |-  ( ph -> C e. ThinCat )
18 4 oppcthin 
 |-  ( C e. ThinCat -> O e. ThinCat )
19 17 18 syl 
 |-  ( ph -> O e. ThinCat )
20 f1oi 
 |-  ( _I |` ( Base ` D ) ) : ( Base ` D ) -1-1-onto-> ( Base ` D )
21 1 2 3 4 oduoppcbas 
 |-  ( ph -> ( Base ` D ) = ( Base ` O ) )
22 21 f1oeq3d 
 |-  ( ph -> ( ( _I |` ( Base ` D ) ) : ( Base ` D ) -1-1-onto-> ( Base ` D ) <-> ( _I |` ( Base ` D ) ) : ( Base ` D ) -1-1-onto-> ( Base ` O ) ) )
23 20 22 mpbii 
 |-  ( ph -> ( _I |` ( Base ` D ) ) : ( Base ` D ) -1-1-onto-> ( Base ` O ) )
24 eqid 
 |-  ( le ` K ) = ( le ` K )
25 eqid 
 |-  ( le ` ( ODual ` K ) ) = ( le ` ( ODual ` K ) )
26 13 24 25 oduleg 
 |-  ( ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) -> ( x ( le ` ( ODual ` K ) ) y <-> y ( le ` K ) x ) )
27 26 adantl 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( x ( le ` ( ODual ` K ) ) y <-> y ( le ` K ) x ) )
28 3 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> D = ( ProsetToCat ` ( ODual ` K ) ) )
29 2 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> K e. Proset )
30 29 14 syl 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( ODual ` K ) e. Proset )
31 eqidd 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( le ` ( ODual ` K ) ) = ( le ` ( ODual ` K ) ) )
32 28 30 31 prstcleval 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( le ` ( ODual ` K ) ) = ( le ` D ) )
33 eqidd 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( Hom ` D ) = ( Hom ` D ) )
34 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> x e. ( Base ` D ) )
35 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> y e. ( Base ` D ) )
36 28 30 32 33 34 35 prstchom 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( x ( le ` ( ODual ` K ) ) y <-> ( x ( Hom ` D ) y ) =/= (/) ) )
37 1 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> C = ( ProsetToCat ` K ) )
38 eqidd 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( le ` K ) = ( le ` K ) )
39 37 29 38 prstcleval 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( le ` K ) = ( le ` C ) )
40 eqidd 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( Hom ` C ) = ( Hom ` C ) )
41 eqid 
 |-  ( Base ` C ) = ( Base ` C )
42 4 41 oppcbas 
 |-  ( Base ` C ) = ( Base ` O )
43 21 42 eqtr4di 
 |-  ( ph -> ( Base ` D ) = ( Base ` C ) )
44 43 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( Base ` D ) = ( Base ` C ) )
45 35 44 eleqtrd 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> y e. ( Base ` C ) )
46 34 44 eleqtrd 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> x e. ( Base ` C ) )
47 37 29 39 40 45 46 prstchom 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( y ( le ` K ) x <-> ( y ( Hom ` C ) x ) =/= (/) ) )
48 27 36 47 3bitr3d 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( ( x ( Hom ` D ) y ) =/= (/) <-> ( y ( Hom ` C ) x ) =/= (/) ) )
49 48 necon4bid 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( ( x ( Hom ` D ) y ) = (/) <-> ( y ( Hom ` C ) x ) = (/) ) )
50 fvresi 
 |-  ( x e. ( Base ` D ) -> ( ( _I |` ( Base ` D ) ) ` x ) = x )
51 50 ad2antrl 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( ( _I |` ( Base ` D ) ) ` x ) = x )
52 fvresi 
 |-  ( y e. ( Base ` D ) -> ( ( _I |` ( Base ` D ) ) ` y ) = y )
53 52 ad2antll 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( ( _I |` ( Base ` D ) ) ` y ) = y )
54 51 53 oveq12d 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( 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 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( ( ( _I |` ( Base ` D ) ) ` x ) ( Hom ` O ) ( ( _I |` ( Base ` D ) ) ` y ) ) = ( y ( Hom ` C ) x ) )
58 57 eqeq1d 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( ( ( ( _I |` ( Base ` D ) ) ` x ) ( Hom ` O ) ( ( _I |` ( Base ` D ) ) ` y ) ) = (/) <-> ( y ( Hom ` C ) x ) = (/) ) )
59 49 58 bitr4d 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( 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 
 |-  ( ph -> D ( ~=c ` ( CatCat ` U ) ) O )