Theorem 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	⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
	prstcnid.k	⊢ ( 𝜑 → 𝐾 ∈ Proset )
	prstchom.l	⊢ ( 𝜑 → ≤ = ( le ‘ 𝐶 ) )
	prstchom.e	⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
	prstchom.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
	prstchom.y	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
Assertion	prstchom	⊢ ( 𝜑 → ( 𝑋 ≤ 𝑌 ↔ ( 𝑋 𝐻 𝑌 ) ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		prstcnid.c	⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
2		prstcnid.k	⊢ ( 𝜑 → 𝐾 ∈ Proset )
3		prstchom.l	⊢ ( 𝜑 → ≤ = ( le ‘ 𝐶 ) )
4		prstchom.e	⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
5		prstchom.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
6		prstchom.y	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
7	1 2 3	prstchomval	⊢ ( 𝜑 → ( ≤ × { 1o } ) = ( Hom ‘ 𝐶 ) )
8	4 7	eqtr4d	⊢ ( 𝜑 → 𝐻 = ( ≤ × { 1o } ) )
9		1oex	⊢ 1o ∈ V
10	9	a1i	⊢ ( 𝜑 → 1o ∈ V )
11		1n0	⊢ 1o ≠ ∅
12	11	a1i	⊢ ( 𝜑 → 1o ≠ ∅ )
13	8 10 12	fvconstrn0	⊢ ( 𝜑 → ( 𝑋 ≤ 𝑌 ↔ ( 𝑋 𝐻 𝑌 ) ≠ ∅ ) )