prstchom

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 . However, this should not be assumed as it is definition-dependent. Therefore, the two hypotheses are added for explicitness. (Contributed by Zhi Wang, 20-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	prstchom	$⊢ φ \to (X \underset{˙}{\leq} Y \leftrightarrow X H Y \neq \emptyset)$

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	prstchomval	$⊢ φ \to \underset{˙}{\leq} \times \{1_{𝑜}\} = Hom (C)$
8	4 7	eqtr4d	$⊢ φ \to H = \underset{˙}{\leq} \times \{1_{𝑜}\}$
9		1oex	$⊢ 1_{𝑜} \in V$
10	9	a1i	$⊢ φ \to 1_{𝑜} \in V$
11		1n0	$⊢ 1_{𝑜} \neq \emptyset$
12	11	a1i	$⊢ φ \to 1_{𝑜} \neq \emptyset$
13	8 10 12	fvconstrn0	$⊢ φ \to (X \underset{˙}{\leq} Y \leftrightarrow X H Y \neq \emptyset)$

Metamath Proof Explorer

Theorem prstchom

Proof