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 ( 𝜑𝐶 = ( ProsetToCat ‘ 𝐾 ) )
prstcnid.k ( 𝜑𝐾 ∈ Proset )
oduoppcbas.d ( 𝜑𝐷 = ( ProsetToCat ‘ ( ODual ‘ 𝐾 ) ) )
oduoppcbas.o 𝑂 = ( oppCat ‘ 𝐶 )
oduoppcciso.u ( 𝜑𝑈𝑉 )
oduoppcciso.d ( 𝜑𝐷𝑈 )
oduoppcciso.o ( 𝜑𝑂𝑈 )
Assertion oduoppcciso ( 𝜑𝐷 ( ≃𝑐 ‘ ( CatCat ‘ 𝑈 ) ) 𝑂 )

Proof

Step Hyp Ref Expression
1 prstcnid.c ( 𝜑𝐶 = ( ProsetToCat ‘ 𝐾 ) )
2 prstcnid.k ( 𝜑𝐾 ∈ Proset )
3 oduoppcbas.d ( 𝜑𝐷 = ( ProsetToCat ‘ ( ODual ‘ 𝐾 ) ) )
4 oduoppcbas.o 𝑂 = ( oppCat ‘ 𝐶 )
5 oduoppcciso.u ( 𝜑𝑈𝑉 )
6 oduoppcciso.d ( 𝜑𝐷𝑈 )
7 oduoppcciso.o ( 𝜑𝑂𝑈 )
8 eqid ( CatCat ‘ 𝑈 ) = ( CatCat ‘ 𝑈 )
9 eqid ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
10 eqid ( Base ‘ 𝑂 ) = ( Base ‘ 𝑂 )
11 eqid ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
12 eqid ( Hom ‘ 𝑂 ) = ( Hom ‘ 𝑂 )
13 eqid ( ODual ‘ 𝐾 ) = ( ODual ‘ 𝐾 )
14 13 oduprs ( 𝐾 ∈ Proset → ( ODual ‘ 𝐾 ) ∈ Proset )
15 2 14 syl ( 𝜑 → ( ODual ‘ 𝐾 ) ∈ Proset )
16 3 15 prstcthin ( 𝜑𝐷 ∈ ThinCat )
17 1 2 prstcthin ( 𝜑𝐶 ∈ ThinCat )
18 4 oppcthin ( 𝐶 ∈ ThinCat → 𝑂 ∈ ThinCat )
19 17 18 syl ( 𝜑𝑂 ∈ ThinCat )
20 f1oi ( I ↾ ( Base ‘ 𝐷 ) ) : ( Base ‘ 𝐷 ) –1-1-onto→ ( Base ‘ 𝐷 )
21 1 2 3 4 oduoppcbas ( 𝜑 → ( Base ‘ 𝐷 ) = ( Base ‘ 𝑂 ) )
22 21 f1oeq3d ( 𝜑 → ( ( I ↾ ( Base ‘ 𝐷 ) ) : ( Base ‘ 𝐷 ) –1-1-onto→ ( Base ‘ 𝐷 ) ↔ ( I ↾ ( Base ‘ 𝐷 ) ) : ( Base ‘ 𝐷 ) –1-1-onto→ ( Base ‘ 𝑂 ) ) )
23 20 22 mpbii ( 𝜑 → ( I ↾ ( Base ‘ 𝐷 ) ) : ( Base ‘ 𝐷 ) –1-1-onto→ ( Base ‘ 𝑂 ) )
24 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
25 eqid ( le ‘ ( ODual ‘ 𝐾 ) ) = ( le ‘ ( ODual ‘ 𝐾 ) )
26 13 24 25 oduleg ( ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑥 ( le ‘ ( ODual ‘ 𝐾 ) ) 𝑦𝑦 ( le ‘ 𝐾 ) 𝑥 ) )
27 26 adantl ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑥 ( le ‘ ( ODual ‘ 𝐾 ) ) 𝑦𝑦 ( le ‘ 𝐾 ) 𝑥 ) )
28 3 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝐷 = ( ProsetToCat ‘ ( ODual ‘ 𝐾 ) ) )
29 2 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝐾 ∈ Proset )
30 29 14 syl ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( ODual ‘ 𝐾 ) ∈ Proset )
31 eqidd ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( le ‘ ( ODual ‘ 𝐾 ) ) = ( le ‘ ( ODual ‘ 𝐾 ) ) )
32 28 30 31 prstcleval ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( le ‘ ( ODual ‘ 𝐾 ) ) = ( le ‘ 𝐷 ) )
33 eqidd ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 ) )
34 simprl ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐷 ) )
35 simprr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐷 ) )
36 28 30 32 33 34 35 prstchom ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑥 ( le ‘ ( ODual ‘ 𝐾 ) ) 𝑦 ↔ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ≠ ∅ ) )
37 1 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
38 eqidd ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) )
39 37 29 38 prstcleval ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( le ‘ 𝐾 ) = ( le ‘ 𝐶 ) )
40 eqidd ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) )
41 eqid ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
42 4 41 oppcbas ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 )
43 21 42 eqtr4di ( 𝜑 → ( Base ‘ 𝐷 ) = ( Base ‘ 𝐶 ) )
44 43 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( Base ‘ 𝐷 ) = ( Base ‘ 𝐶 ) )
45 35 44 eleqtrd ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
46 34 44 eleqtrd ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
47 37 29 39 40 45 46 prstchom ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑦 ( le ‘ 𝐾 ) 𝑥 ↔ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ≠ ∅ ) )
48 27 36 47 3bitr3d ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ≠ ∅ ↔ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ≠ ∅ ) )
49 48 necon4bid ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) = ∅ ↔ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) = ∅ ) )
50 fvresi ( 𝑥 ∈ ( Base ‘ 𝐷 ) → ( ( I ↾ ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) = 𝑥 )
51 50 ad2antrl ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( ( I ↾ ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) = 𝑥 )
52 fvresi ( 𝑦 ∈ ( Base ‘ 𝐷 ) → ( ( I ↾ ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) = 𝑦 )
53 52 ad2antll ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( ( I ↾ ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) = 𝑦 )
54 51 53 oveq12d ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( ( ( I ↾ ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝑂 ) ( ( I ↾ ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) = ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) )
55 eqid ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
56 55 4 oppchom ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 )
57 54 56 eqtrdi ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( ( ( I ↾ ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝑂 ) ( ( I ↾ ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) = ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) )
58 57 eqeq1d ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( ( ( ( I ↾ ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝑂 ) ( ( I ↾ ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) = ∅ ↔ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) = ∅ ) )
59 49 58 bitr4d ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) = ∅ ↔ ( ( ( I ↾ ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝑂 ) ( ( I ↾ ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) = ∅ ) )
60 8 9 10 11 12 5 6 7 16 19 23 59 thinccisod ( 𝜑𝐷 ( ≃𝑐 ‘ ( CatCat ‘ 𝑈 ) ) 𝑂 )