thincciso

Description: Two thin categories are isomorphic iff the induced preorders are order-isomorphic. Example 3.26(2) of Adamek p. 33. Note that "thincciso.u" is redundant thanks to elbasfv . (Contributed by Zhi Wang, 16-Oct-2024)

	Ref	Expression
Hypotheses	thincciso.c	$⊢ C = CatCat (U)$
	thincciso.b	$⊢ B = {Base}_{C}$
	thincciso.r	$⊢ R = {Base}_{X}$
	thincciso.s	$⊢ S = {Base}_{Y}$
	thincciso.h	$⊢ H = Hom (X)$
	thincciso.j	$⊢ J = Hom (Y)$
	thincciso.u	$⊢ φ \to U \in V$
	thincciso.x	$⊢ φ \to X \in B$
	thincciso.y	$⊢ φ \to Y \in B$
	thincciso.xt	$⊢ φ \to X \in ThinCat$
	thincciso.yt	$⊢ φ \to Y \in ThinCat$
Assertion	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))$

Proof

Step	Hyp	Ref	Expression
1		thincciso.c	$⊢ C = CatCat (U)$
2		thincciso.b	$⊢ B = {Base}_{C}$
3		thincciso.r	$⊢ R = {Base}_{X}$
4		thincciso.s	$⊢ S = {Base}_{Y}$
5		thincciso.h	$⊢ H = Hom (X)$
6		thincciso.j	$⊢ J = Hom (Y)$
7		thincciso.u	$⊢ φ \to U \in V$
8		thincciso.x	$⊢ φ \to X \in B$
9		thincciso.y	$⊢ φ \to Y \in B$
10		thincciso.xt	$⊢ φ \to X \in ThinCat$
11		thincciso.yt	$⊢ φ \to Y \in ThinCat$
12		eqid	$⊢ Iso (C) = Iso (C)$
13	1	catccat	$⊢ U \in V \to C \in Cat$
14	7 13	syl	$⊢ φ \to C \in Cat$
15	12 2 14 8 9	cic	$⊢ φ \to (X ≃_{𝑐} (C) Y \leftrightarrow \exists a a \in (X Iso (C) Y))$
16		opex	$⊢ ⟨f, (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))⟩ \in V$
17	16	a1i	$⊢ (φ \land (\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)) \to ⟨f, (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))⟩ \in V$
18		biimp	$⊢ (x H y = \emptyset \leftrightarrow f (x) J f (y) = \emptyset) \to (x H y = \emptyset \to f (x) J f (y) = \emptyset)$
19	18	2ralimi	$⊢ \forall x \in R \forall y \in R (x H y = \emptyset \leftrightarrow f (x) J f (y) = \emptyset) \to \forall x \in R \forall y \in R (x H y = \emptyset \to f (x) J f (y) = \emptyset)$
20	19	ad2antrl	$⊢ (φ \land (\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)) \to \forall x \in R \forall y \in R (x H y = \emptyset \to f (x) J f (y) = \emptyset)$
21	11	adantr	$⊢ (φ \land (\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)) \to Y \in ThinCat$
22		eqid	$⊢ (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w))) = (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))$
23	10	adantr	$⊢ (φ \land (\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)) \to X \in ThinCat$
24	23	thinccatd	$⊢ (φ \land (\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)) \to X \in Cat$
25		simprr	$⊢ (φ \land (\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)) \to f : R \underset{1-1 onto}{⟶} S$
26		f1of	$⊢ f : R \underset{1-1 onto}{⟶} S \to f : R ⟶ S$
27	25 26	syl	$⊢ (φ \land (\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)) \to f : R ⟶ S$
28		biimpr	$⊢ (x H y = \emptyset \leftrightarrow f (x) J f (y) = \emptyset) \to (f (x) J f (y) = \emptyset \to x H y = \emptyset)$
29	28	2ralimi	$⊢ \forall x \in R \forall y \in R (x H y = \emptyset \leftrightarrow f (x) J f (y) = \emptyset) \to \forall x \in R \forall y \in R (f (x) J f (y) = \emptyset \to x H y = \emptyset)$
30	29	ad2antrl	$⊢ (φ \land (\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)) \to \forall x \in R \forall y \in R (f (x) J f (y) = \emptyset \to x H y = \emptyset)$
31	3 4 5 6 24 21 27 22 30	functhinc	$⊢ (φ \land (\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)) \to (f (X Func Y) (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w))) \leftrightarrow (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w))) = (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w))))$
32	22 31	mpbiri	$⊢ (φ \land (\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)) \to f (X Func Y) (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))$
33	3 6 5 21 32	fullthinc	$⊢ (φ \land (\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)) \to (f (X Full Y) (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w))) \leftrightarrow \forall x \in R \forall y \in R (x H y = \emptyset \to f (x) J f (y) = \emptyset))$
34	20 33	mpbird	$⊢ (φ \land (\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)) \to f (X Full Y) (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))$
35		df-br	$⊢ f (X Full Y) (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w))) \leftrightarrow ⟨f, (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))⟩ \in (X Full Y)$
36	34 35	sylib	$⊢ (φ \land (\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)) \to ⟨f, (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))⟩ \in (X Full Y)$
37	23 32	thincfth	$⊢ (φ \land (\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)) \to f (X Faith Y) (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))$
38		df-br	$⊢ f (X Faith Y) (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w))) \leftrightarrow ⟨f, (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))⟩ \in (X Faith Y)$
39	37 38	sylib	$⊢ (φ \land (\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)) \to ⟨f, (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))⟩ \in (X Faith Y)$
40	36 39	elind	$⊢ (φ \land (\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)) \to ⟨f, (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))⟩ \in ((X Full Y) \cap (X Faith Y))$
41		vex	$⊢ f \in V$
42	3	fvexi	$⊢ R \in V$
43	42 42	mpoex	$⊢ (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w))) \in V$
44	41 43	op1st	$⊢ 1^{st} (⟨f, (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))⟩) = f$
45		f1oeq1	$⊢ 1^{st} (⟨f, (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))⟩) = f \to (1^{st} (⟨f, (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))⟩) : R \underset{1-1 onto}{⟶} S \leftrightarrow f : R \underset{1-1 onto}{⟶} S)$
46	44 45	ax-mp	$⊢ 1^{st} (⟨f, (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))⟩) : R \underset{1-1 onto}{⟶} S \leftrightarrow f : R \underset{1-1 onto}{⟶} S$
47	25 46	sylibr	$⊢ (φ \land (\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)) \to 1^{st} (⟨f, (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))⟩) : R \underset{1-1 onto}{⟶} S$
48	40 47	jca	$⊢ (φ \land (\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)) \to (⟨f, (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))⟩ \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (⟨f, (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))⟩) : R \underset{1-1 onto}{⟶} S)$
49	1 2 3 4 7 8 9 12	catciso	$⊢ φ \to (⟨f, (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))⟩ \in (X Iso (C) Y) \leftrightarrow (⟨f, (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))⟩ \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (⟨f, (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))⟩) : R \underset{1-1 onto}{⟶} S))$
50	49	biimpar	$⊢ (φ \land (⟨f, (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))⟩ \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (⟨f, (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))⟩) : R \underset{1-1 onto}{⟶} S)) \to ⟨f, (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))⟩ \in (X Iso (C) Y)$
51	48 50	syldan	$⊢ (φ \land (\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)) \to ⟨f, (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))⟩ \in (X Iso (C) Y)$
52		eleq1	$⊢ a = ⟨f, (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))⟩ \to (a \in (X Iso (C) Y) \leftrightarrow ⟨f, (z \in R, w \in R ⟼ (z H w) \times (f (z) J f (w)))⟩ \in (X Iso (C) Y))$
53	17 51 52	spcedv	$⊢ (φ \land (\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)) \to \exists a a \in (X Iso (C) Y)$
54	53	ex	$⊢ φ \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) \to \exists a a \in (X Iso (C) Y))$
55	54	exlimdv	$⊢ φ \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) \to \exists a a \in (X Iso (C) Y))$
56		fvexd	$⊢ (φ \land a \in (X Iso (C) Y)) \to 1^{st} (a) \in V$
57		relfull	$⊢ Rel (X Full Y)$
58	1 2 3 4 7 8 9 12	catciso	$⊢ φ \to (a \in (X Iso (C) Y) \leftrightarrow (a \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (a) : R \underset{1-1 onto}{⟶} S))$
59	58	biimpa	$⊢ (φ \land a \in (X Iso (C) Y)) \to (a \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (a) : R \underset{1-1 onto}{⟶} S)$
60	59	simpld	$⊢ (φ \land a \in (X Iso (C) Y)) \to a \in ((X Full Y) \cap (X Faith Y))$
61	60	elin1d	$⊢ (φ \land a \in (X Iso (C) Y)) \to a \in (X Full Y)$
62		1st2ndbr	$⊢ (Rel (X Full Y) \land a \in (X Full Y)) \to 1^{st} (a) (X Full Y) 2^{nd} (a)$
63	57 61 62	sylancr	$⊢ (φ \land a \in (X Iso (C) Y)) \to 1^{st} (a) (X Full Y) 2^{nd} (a)$
64	11	adantr	$⊢ (φ \land a \in (X Iso (C) Y)) \to Y \in ThinCat$
65		fullfunc	$⊢ X Full Y \subseteq X Func Y$
66	65	ssbri	$⊢ 1^{st} (a) (X Full Y) 2^{nd} (a) \to 1^{st} (a) (X Func Y) 2^{nd} (a)$
67	63 66	syl	$⊢ (φ \land a \in (X Iso (C) Y)) \to 1^{st} (a) (X Func Y) 2^{nd} (a)$
68	3 6 5 64 67	fullthinc	$⊢ (φ \land a \in (X Iso (C) Y)) \to (1^{st} (a) (X Full Y) 2^{nd} (a) \leftrightarrow \forall x \in R \forall y \in R (x H y = \emptyset \to 1^{st} (a) (x) J 1^{st} (a) (y) = \emptyset))$
69	63 68	mpbid	$⊢ (φ \land a \in (X Iso (C) Y)) \to \forall x \in R \forall y \in R (x H y = \emptyset \to 1^{st} (a) (x) J 1^{st} (a) (y) = \emptyset)$
70	67	adantr	$⊢ ((φ \land a \in (X Iso (C) Y)) \land (x \in R \land y \in R)) \to 1^{st} (a) (X Func Y) 2^{nd} (a)$
71		simprl	$⊢ ((φ \land a \in (X Iso (C) Y)) \land (x \in R \land y \in R)) \to x \in R$
72		simprr	$⊢ ((φ \land a \in (X Iso (C) Y)) \land (x \in R \land y \in R)) \to y \in R$
73	3 5 6 70 71 72	funcf2	$⊢ ((φ \land a \in (X Iso (C) Y)) \land (x \in R \land y \in R)) \to (x 2^{nd} (a) y) : x H y ⟶ 1^{st} (a) (x) J 1^{st} (a) (y)$
74	73	f002	$⊢ ((φ \land a \in (X Iso (C) Y)) \land (x \in R \land y \in R)) \to (1^{st} (a) (x) J 1^{st} (a) (y) = \emptyset \to x H y = \emptyset)$
75	74	ralrimivva	$⊢ (φ \land a \in (X Iso (C) Y)) \to \forall x \in R \forall y \in R (1^{st} (a) (x) J 1^{st} (a) (y) = \emptyset \to x H y = \emptyset)$
76		2ralbiim	$⊢ \forall x \in R \forall y \in R (x H y = \emptyset \leftrightarrow 1^{st} (a) (x) J 1^{st} (a) (y) = \emptyset) \leftrightarrow (\forall x \in R \forall y \in R (x H y = \emptyset \to 1^{st} (a) (x) J 1^{st} (a) (y) = \emptyset) \land \forall x \in R \forall y \in R (1^{st} (a) (x) J 1^{st} (a) (y) = \emptyset \to x H y = \emptyset))$
77	69 75 76	sylanbrc	$⊢ (φ \land a \in (X Iso (C) Y)) \to \forall x \in R \forall y \in R (x H y = \emptyset \leftrightarrow 1^{st} (a) (x) J 1^{st} (a) (y) = \emptyset)$
78	59	simprd	$⊢ (φ \land a \in (X Iso (C) Y)) \to 1^{st} (a) : R \underset{1-1 onto}{⟶} S$
79	77 78	jca	$⊢ (φ \land a \in (X Iso (C) Y)) \to (\forall x \in R \forall y \in R (x H y = \emptyset \leftrightarrow 1^{st} (a) (x) J 1^{st} (a) (y) = \emptyset) \land 1^{st} (a) : R \underset{1-1 onto}{⟶} S)$
80		fveq1	$⊢ f = 1^{st} (a) \to f (x) = 1^{st} (a) (x)$
81		fveq1	$⊢ f = 1^{st} (a) \to f (y) = 1^{st} (a) (y)$
82	80 81	oveq12d	$⊢ f = 1^{st} (a) \to f (x) J f (y) = 1^{st} (a) (x) J 1^{st} (a) (y)$
83	82	eqeq1d	$⊢ f = 1^{st} (a) \to (f (x) J f (y) = \emptyset \leftrightarrow 1^{st} (a) (x) J 1^{st} (a) (y) = \emptyset)$
84	83	bibi2d	$⊢ f = 1^{st} (a) \to ((x H y = \emptyset \leftrightarrow f (x) J f (y) = \emptyset) \leftrightarrow (x H y = \emptyset \leftrightarrow 1^{st} (a) (x) J 1^{st} (a) (y) = \emptyset))$
85	84	2ralbidv	$⊢ f = 1^{st} (a) \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 1^{st} (a) (x) J 1^{st} (a) (y) = \emptyset))$
86		f1oeq1	$⊢ f = 1^{st} (a) \to (f : R \underset{1-1 onto}{⟶} S \leftrightarrow 1^{st} (a) : R \underset{1-1 onto}{⟶} S)$
87	85 86	anbi12d	$⊢ f = 1^{st} (a) \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 1^{st} (a) (x) J 1^{st} (a) (y) = \emptyset) \land 1^{st} (a) : R \underset{1-1 onto}{⟶} S))$
88	56 79 87	spcedv	$⊢ (φ \land a \in (X Iso (C) Y)) \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)$
89	88	ex	$⊢ φ \to (a \in (X Iso (C) Y) \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))$
90	89	exlimdv	$⊢ φ \to (\exists a a \in (X Iso (C) Y) \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))$
91	55 90	impbid	$⊢ φ \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) \leftrightarrow \exists a a \in (X Iso (C) Y))$
92	15 91	bitr4d	$⊢ φ \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))$

Metamath Proof Explorer

Theorem thincciso

Proof