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 ‘ 𝑈 ) ) 𝑂 )