postc

Description: The converted category is a poset iff no distinct objects are isomorphic. (Contributed by Zhi Wang, 25-Sep-2024)

	Ref	Expression
Hypotheses	postc.c	No typesetting found for \|- ( ph -> C = ( ProsetToCat ` K ) ) with typecode \|-
	postc.k	$⊢ φ \to K \in Proset$
	postc.b	$⊢ B = {Base}_{C}$
Assertion	postc	$⊢ φ \to (C \in Poset \leftrightarrow \forall x \in B \forall y \in B (x ≃_{𝑐} (C) y \to x = y))$

Proof

Step	Hyp	Ref	Expression
1		postc.c	Could not format ( ph -> C = ( ProsetToCat ` K ) ) : No typesetting found for \|- ( ph -> C = ( ProsetToCat ` K ) ) with typecode \|-
2		postc.k	$⊢ φ \to K \in Proset$
3		postc.b	$⊢ B = {Base}_{C}$
4	1 2	prstcprs	$⊢ φ \to C \in Proset$
5		eqid	$⊢ \leq_{C} = \leq_{C}$
6	3 5	ispos2	$⊢ C \in Poset \leftrightarrow (C \in Proset \land \forall x \in B \forall y \in B ((x \leq_{C} y \land y \leq_{C} x) \to x = y))$
7	6	baib	$⊢ C \in Proset \to (C \in Poset \leftrightarrow \forall x \in B \forall y \in B ((x \leq_{C} y \land y \leq_{C} x) \to x = y))$
8	4 7	syl	$⊢ φ \to (C \in Poset \leftrightarrow \forall x \in B \forall y \in B ((x \leq_{C} y \land y \leq_{C} x) \to x = y))$
9	1	adantr	Could not format ( ( ph /\ ( x e. B /\ y e. B ) ) -> C = ( ProsetToCat ` K ) ) : No typesetting found for \|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> C = ( ProsetToCat ` K ) ) with typecode \|-
10	2	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to K \in Proset$
11	9 10	prstcthin	Could not format ( ( ph /\ ( x e. B /\ y e. B ) ) -> C e. ThinCat ) : No typesetting found for \|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> C e. ThinCat ) with typecode \|-
12		simprl	$⊢ (φ \land (x \in B \land y \in B)) \to x \in B$
13		simprr	$⊢ (φ \land (x \in B \land y \in B)) \to y \in B$
14		eqid	$⊢ Hom (C) = Hom (C)$
15	11 3 12 13 14	thinccic	$⊢ (φ \land (x \in B \land y \in B)) \to (x ≃_{𝑐} (C) y \leftrightarrow (x Hom (C) y \neq \emptyset \land y Hom (C) x \neq \emptyset))$
16		eqidd	$⊢ (φ \land (x \in B \land y \in B)) \to \leq_{C} = \leq_{C}$
17		eqidd	$⊢ (φ \land (x \in B \land y \in B)) \to Hom (C) = Hom (C)$
18	12 3	eleqtrdi	$⊢ (φ \land (x \in B \land y \in B)) \to x \in {Base}_{C}$
19	13 3	eleqtrdi	$⊢ (φ \land (x \in B \land y \in B)) \to y \in {Base}_{C}$
20	9 10 16 17 18 19	prstchom	$⊢ (φ \land (x \in B \land y \in B)) \to (x \leq_{C} y \leftrightarrow x Hom (C) y \neq \emptyset)$
21	9 10 16 17 19 18	prstchom	$⊢ (φ \land (x \in B \land y \in B)) \to (y \leq_{C} x \leftrightarrow y Hom (C) x \neq \emptyset)$
22	20 21	anbi12d	$⊢ (φ \land (x \in B \land y \in B)) \to ((x \leq_{C} y \land y \leq_{C} x) \leftrightarrow (x Hom (C) y \neq \emptyset \land y Hom (C) x \neq \emptyset))$
23	15 22	bitr4d	$⊢ (φ \land (x \in B \land y \in B)) \to (x ≃_{𝑐} (C) y \leftrightarrow (x \leq_{C} y \land y \leq_{C} x))$
24	23	imbi1d	$⊢ (φ \land (x \in B \land y \in B)) \to ((x ≃_{𝑐} (C) y \to x = y) \leftrightarrow ((x \leq_{C} y \land y \leq_{C} x) \to x = y))$
25	24	2ralbidva	$⊢ φ \to (\forall x \in B \forall y \in B (x ≃_{𝑐} (C) y \to x = y) \leftrightarrow \forall x \in B \forall y \in B ((x \leq_{C} y \land y \leq_{C} x) \to x = y))$
26	8 25	bitr4d	$⊢ φ \to (C \in Poset \leftrightarrow \forall x \in B \forall y \in B (x ≃_{𝑐} (C) y \to x = y))$

Metamath Proof Explorer

Theorem postc

Proof