thinccisod

Description: Two thin categories are isomorphic if the induced preorders are order-isomorphic (deduction form). Example 3.26(2) of Adamek p. 33. (Contributed by Zhi Wang, 22-Sep-2025)

	Ref	Expression
Hypotheses	thinccisod.c	$⊢ C = CatCat (U)$
	thinccisod.r	$⊢ R = {Base}_{X}$
	thinccisod.s	$⊢ S = {Base}_{Y}$
	thinccisod.h	$⊢ H = Hom (X)$
	thinccisod.j	$⊢ J = Hom (Y)$
	thinccisod.u	$⊢ φ \to U \in V$
	thinccisod.x	$⊢ φ \to X \in U$
	thinccisod.y	$⊢ φ \to Y \in U$
	thinccisod.xt	$⊢ φ \to X \in ThinCat$
	thinccisod.yt	$⊢ φ \to Y \in ThinCat$
	thinccisod.f	$⊢ φ \to F : R \underset{1-1 onto}{⟶} S$
	thinccisod.1	$⊢ (φ \land (x \in R \land y \in R)) \to (x H y = \emptyset \leftrightarrow F (x) J F (y) = \emptyset)$
Assertion	thinccisod	$⊢ φ \to X ≃_{𝑐} (C) Y$

Proof

Step	Hyp	Ref	Expression
1		thinccisod.c	$⊢ C = CatCat (U)$
2		thinccisod.r	$⊢ R = {Base}_{X}$
3		thinccisod.s	$⊢ S = {Base}_{Y}$
4		thinccisod.h	$⊢ H = Hom (X)$
5		thinccisod.j	$⊢ J = Hom (Y)$
6		thinccisod.u	$⊢ φ \to U \in V$
7		thinccisod.x	$⊢ φ \to X \in U$
8		thinccisod.y	$⊢ φ \to Y \in U$
9		thinccisod.xt	$⊢ φ \to X \in ThinCat$
10		thinccisod.yt	$⊢ φ \to Y \in ThinCat$
11		thinccisod.f	$⊢ φ \to F : R \underset{1-1 onto}{⟶} S$
12		thinccisod.1	$⊢ (φ \land (x \in R \land y \in R)) \to (x H y = \emptyset \leftrightarrow F (x) J F (y) = \emptyset)$
13		f1of	$⊢ F : R \underset{1-1 onto}{⟶} S \to F : R ⟶ S$
14	11 13	syl	$⊢ φ \to F : R ⟶ S$
15		fvexd	$⊢ φ \to {Base}_{X} \in V$
16	2 15	eqeltrid	$⊢ φ \to R \in V$
17	14 16	fexd	$⊢ φ \to F \in V$
18	12	ralrimivva	$⊢ φ \to \forall x \in R \forall y \in R (x H y = \emptyset \leftrightarrow F (x) J F (y) = \emptyset)$
19	18 11	jca	$⊢ φ \to (\forall x \in R \forall y \in R (x H y = \emptyset \leftrightarrow F (x) J F (y) = \emptyset) \land F : R \underset{1-1 onto}{⟶} S)$
20		fveq1	$⊢ f = F \to f (x) = F (x)$
21		fveq1	$⊢ f = F \to f (y) = F (y)$
22	20 21	oveq12d	$⊢ f = F \to f (x) J f (y) = F (x) J F (y)$
23	22	eqeq1d	$⊢ f = F \to (f (x) J f (y) = \emptyset \leftrightarrow F (x) J F (y) = \emptyset)$
24	23	bibi2d	$⊢ f = F \to ((x H y = \emptyset \leftrightarrow f (x) J f (y) = \emptyset) \leftrightarrow (x H y = \emptyset \leftrightarrow F (x) J F (y) = \emptyset))$
25	24	2ralbidv	$⊢ f = F \to (\forall x \in R \forall y \in R (x H y = \emptyset \leftrightarrow f (x) J f (y) = \emptyset) \leftrightarrow \forall x \in R \forall y \in R (x H y = \emptyset \leftrightarrow F (x) J F (y) = \emptyset))$
26		f1oeq1	$⊢ f = F \to (f : R \underset{1-1 onto}{⟶} S \leftrightarrow F : R \underset{1-1 onto}{⟶} S)$
27	25 26	anbi12d	$⊢ f = F \to ((\forall x \in R \forall y \in R (x H y = \emptyset \leftrightarrow f (x) J f (y) = \emptyset) \land f : R \underset{1-1 onto}{⟶} S) \leftrightarrow (\forall x \in R \forall y \in R (x H y = \emptyset \leftrightarrow F (x) J F (y) = \emptyset) \land F : R \underset{1-1 onto}{⟶} S))$
28	17 19 27	spcedv	$⊢ φ \to \exists f (\forall x \in R \forall y \in R (x H y = \emptyset \leftrightarrow f (x) J f (y) = \emptyset) \land f : R \underset{1-1 onto}{⟶} S)$
29		eqid	$⊢ {Base}_{C} = {Base}_{C}$
30	9	thinccatd	$⊢ φ \to X \in Cat$
31	7 30	elind	$⊢ φ \to X \in (U \cap Cat)$
32	1 29 6	catcbas	$⊢ φ \to {Base}_{C} = U \cap Cat$
33	31 32	eleqtrrd	$⊢ φ \to X \in {Base}_{C}$
34	10	thinccatd	$⊢ φ \to Y \in Cat$
35	8 34	elind	$⊢ φ \to Y \in (U \cap Cat)$
36	35 32	eleqtrrd	$⊢ φ \to Y \in {Base}_{C}$
37	1 29 2 3 4 5 6 33 36 9 10	thincciso	$⊢ φ \to (X ≃_{𝑐} (C) Y \leftrightarrow \exists f (\forall x \in R \forall y \in R (x H y = \emptyset \leftrightarrow f (x) J f (y) = \emptyset) \land f : R \underset{1-1 onto}{⟶} S))$
38	28 37	mpbird	$⊢ φ \to X ≃_{𝑐} (C) Y$

Metamath Proof Explorer

Theorem thinccisod

Proof