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	$⊢ φ \to C = ProsetToCat (K)$
	prstcnid.k	$⊢ φ \to K \in Proset$
	oduoppcbas.d	$⊢ φ \to D = ProsetToCat (ODual (K))$
	oduoppcbas.o	$⊢ O = oppCat (C)$
	oduoppcciso.u	$⊢ φ \to U \in V$
	oduoppcciso.d	$⊢ φ \to D \in U$
	oduoppcciso.o	$⊢ φ \to O \in U$
Assertion	oduoppcciso	$⊢ φ \to D ≃_{𝑐} (CatCat (U)) O$

Proof

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

Metamath Proof Explorer

Theorem oduoppcciso

Proof