thinccic

Description: In a thin category, two objects are isomorphic iff there are morphisms between them in both directions. (Contributed by Zhi Wang, 25-Sep-2024)

	Ref	Expression
Hypotheses	thincsect.c	$⊢ φ \to C \in ThinCat$
	thincsect.b	$⊢ B = {Base}_{C}$
	thincsect.x	$⊢ φ \to X \in B$
	thincsect.y	$⊢ φ \to Y \in B$
	thinciso.h	$⊢ H = Hom (C)$
Assertion	thinccic	$⊢ φ \to (X ≃_{𝑐} (C) Y \leftrightarrow (X H Y \neq \emptyset \land Y H X \neq \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		thincsect.c	$⊢ φ \to C \in ThinCat$
2		thincsect.b	$⊢ B = {Base}_{C}$
3		thincsect.x	$⊢ φ \to X \in B$
4		thincsect.y	$⊢ φ \to Y \in B$
5		thinciso.h	$⊢ H = Hom (C)$
6		eqid	$⊢ Iso (C) = Iso (C)$
7	1	thinccatd	$⊢ φ \to C \in Cat$
8	2 5 6 7 3 4	isohom	$⊢ φ \to X Iso (C) Y \subseteq X H Y$
9	8	sselda	$⊢ (φ \land f \in (X Iso (C) Y)) \to f \in (X H Y)$
10	1	adantr	$⊢ (φ \land f \in (X H Y)) \to C \in ThinCat$
11	3	adantr	$⊢ (φ \land f \in (X H Y)) \to X \in B$
12	4	adantr	$⊢ (φ \land f \in (X H Y)) \to Y \in B$
13		simpr	$⊢ (φ \land f \in (X H Y)) \to f \in (X H Y)$
14	10 2 11 12 5 6 13	thinciso	$⊢ (φ \land f \in (X H Y)) \to (f \in (X Iso (C) Y) \leftrightarrow Y H X \neq \emptyset)$
15	9 14	biadanid	$⊢ φ \to (f \in (X Iso (C) Y) \leftrightarrow (f \in (X H Y) \land Y H X \neq \emptyset))$
16	15	exbidv	$⊢ φ \to (\exists f f \in (X Iso (C) Y) \leftrightarrow \exists f (f \in (X H Y) \land Y H X \neq \emptyset))$
17	6 2 7 3 4	cic	$⊢ φ \to (X ≃_{𝑐} (C) Y \leftrightarrow \exists f f \in (X Iso (C) Y))$
18		n0	$⊢ X H Y \neq \emptyset \leftrightarrow \exists f f \in (X H Y)$
19	18	anbi1i	$⊢ (X H Y \neq \emptyset \land Y H X \neq \emptyset) \leftrightarrow (\exists f f \in (X H Y) \land Y H X \neq \emptyset)$
20		19.41v	$⊢ \exists f (f \in (X H Y) \land Y H X \neq \emptyset) \leftrightarrow (\exists f f \in (X H Y) \land Y H X \neq \emptyset)$
21	19 20	bitr4i	$⊢ (X H Y \neq \emptyset \land Y H X \neq \emptyset) \leftrightarrow \exists f (f \in (X H Y) \land Y H X \neq \emptyset)$
22	21	a1i	$⊢ φ \to ((X H Y \neq \emptyset \land Y H X \neq \emptyset) \leftrightarrow \exists f (f \in (X H Y) \land Y H X \neq \emptyset))$
23	16 17 22	3bitr4d	$⊢ φ \to (X ≃_{𝑐} (C) Y \leftrightarrow (X H Y \neq \emptyset \land Y H X \neq \emptyset))$

Metamath Proof Explorer

Theorem thinccic

Proof