thincciso4

Description: Two isomorphic categories are either both thin or neither. Note that "thincciso2.u" is redundant thanks to elbasfv . (Contributed by Zhi Wang, 18-Oct-2025)

	Ref	Expression
Hypotheses	thincciso2.c	$⊢ C = CatCat (U)$
	thincciso2.b	$⊢ B = {Base}_{C}$
	thincciso2.u	$⊢ φ \to U \in V$
	thincciso2.x	$⊢ φ \to X \in B$
	thincciso2.y	$⊢ φ \to Y \in B$
	thincciso4.i	$⊢ φ \to X ≃_{𝑐} (C) Y$
Assertion	thincciso4	$⊢ φ \to (X \in ThinCat \leftrightarrow Y \in ThinCat)$

Proof

Step	Hyp	Ref	Expression
1		thincciso2.c	$⊢ C = CatCat (U)$
2		thincciso2.b	$⊢ B = {Base}_{C}$
3		thincciso2.u	$⊢ φ \to U \in V$
4		thincciso2.x	$⊢ φ \to X \in B$
5		thincciso2.y	$⊢ φ \to Y \in B$
6		thincciso4.i	$⊢ φ \to X ≃_{𝑐} (C) Y$
7		eqid	$⊢ Iso (C) = Iso (C)$
8	1	catccat	$⊢ U \in V \to C \in Cat$
9	3 8	syl	$⊢ φ \to C \in Cat$
10	7 2 9 4 5	cic	$⊢ φ \to (X ≃_{𝑐} (C) Y \leftrightarrow \exists f f \in (X Iso (C) Y))$
11	6 10	mpbid	$⊢ φ \to \exists f f \in (X Iso (C) Y)$
12	11	adantr	$⊢ (φ \land X \in ThinCat) \to \exists f f \in (X Iso (C) Y)$
13	3	ad2antrr	$⊢ ((φ \land X \in ThinCat) \land f \in (X Iso (C) Y)) \to U \in V$
14	4	ad2antrr	$⊢ ((φ \land X \in ThinCat) \land f \in (X Iso (C) Y)) \to X \in B$
15	5	ad2antrr	$⊢ ((φ \land X \in ThinCat) \land f \in (X Iso (C) Y)) \to Y \in B$
16		simpr	$⊢ ((φ \land X \in ThinCat) \land f \in (X Iso (C) Y)) \to f \in (X Iso (C) Y)$
17		simplr	$⊢ ((φ \land X \in ThinCat) \land f \in (X Iso (C) Y)) \to X \in ThinCat$
18	1 2 13 14 15 7 16 17	thincciso3	$⊢ ((φ \land X \in ThinCat) \land f \in (X Iso (C) Y)) \to Y \in ThinCat$
19	12 18	exlimddv	$⊢ (φ \land X \in ThinCat) \to Y \in ThinCat$
20	11	adantr	$⊢ (φ \land Y \in ThinCat) \to \exists f f \in (X Iso (C) Y)$
21	3	ad2antrr	$⊢ ((φ \land Y \in ThinCat) \land f \in (X Iso (C) Y)) \to U \in V$
22	4	ad2antrr	$⊢ ((φ \land Y \in ThinCat) \land f \in (X Iso (C) Y)) \to X \in B$
23	5	ad2antrr	$⊢ ((φ \land Y \in ThinCat) \land f \in (X Iso (C) Y)) \to Y \in B$
24		simpr	$⊢ ((φ \land Y \in ThinCat) \land f \in (X Iso (C) Y)) \to f \in (X Iso (C) Y)$
25		simplr	$⊢ ((φ \land Y \in ThinCat) \land f \in (X Iso (C) Y)) \to Y \in ThinCat$
26	1 2 21 22 23 7 24 25	thincciso2	$⊢ ((φ \land Y \in ThinCat) \land f \in (X Iso (C) Y)) \to X \in ThinCat$
27	20 26	exlimddv	$⊢ (φ \land Y \in ThinCat) \to X \in ThinCat$
28	19 27	impbida	$⊢ φ \to (X \in ThinCat \leftrightarrow Y \in ThinCat)$

Metamath Proof Explorer

Theorem thincciso4

Proof