prstchom2

Description: Hom-sets of the constructed category are dependent on the preorder.

Note that prstchom.x and prstchom.y are redundant here due to our definition of ProsetToCat ( see prstchom2ALT ). However, this should not be assumed as it is definition-dependent. Therefore, the two hypotheses are added for explicitness. (Contributed by Zhi Wang, 21-Sep-2024)

	Ref	Expression
Hypotheses	prstcnid.c	$⊢ φ \to C = ProsetToCat (K)$
	prstcnid.k	$⊢ φ \to K \in Proset$
	prstchom.l	$⊢ φ \to \underset{˙}{\leq} = \leq_{C}$
	prstchom.e	$⊢ φ \to H = Hom (C)$
	prstchom.x	$⊢ φ \to X \in {Base}_{C}$
	prstchom.y	$⊢ φ \to Y \in {Base}_{C}$
Assertion	prstchom2	$⊢ φ \to (X \underset{˙}{\leq} Y \leftrightarrow \exists! f f \in (X H Y))$

Proof

Step	Hyp	Ref	Expression
1		prstcnid.c	$⊢ φ \to C = ProsetToCat (K)$
2		prstcnid.k	$⊢ φ \to K \in Proset$
3		prstchom.l	$⊢ φ \to \underset{˙}{\leq} = \leq_{C}$
4		prstchom.e	$⊢ φ \to H = Hom (C)$
5		prstchom.x	$⊢ φ \to X \in {Base}_{C}$
6		prstchom.y	$⊢ φ \to Y \in {Base}_{C}$
7	1 2 3 4 5 6	prstchom	$⊢ φ \to (X \underset{˙}{\leq} Y \leftrightarrow X H Y \neq \emptyset)$
8	1 2	prstcthin	$⊢ φ \to C \in ThinCat$
9		eqidd	$⊢ φ \to {Base}_{C} = {Base}_{C}$
10	8 5 6 9 4	thincn0eu	$⊢ φ \to (X H Y \neq \emptyset \leftrightarrow \exists! f f \in (X H Y))$
11	7 10	bitrd	$⊢ φ \to (X \underset{˙}{\leq} Y \leftrightarrow \exists! f f \in (X H Y))$

Metamath Proof Explorer

Theorem prstchom2

Proof