Theorem prstchomval

Description: Hom-sets of the constructed category which depend on an arbitrary definition. (Contributed by Zhi Wang, 20-Sep-2024) (New usage is discouraged.)

	Ref	Expression
Hypotheses	prstcnid.c	⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
	prstcnid.k	⊢ ( 𝜑 → 𝐾 ∈ Proset )
	prstchomval.l	⊢ ( 𝜑 → ≤ = ( le ‘ 𝐶 ) )
Assertion	prstchomval	⊢ ( 𝜑 → ( ≤ × { 1o } ) = ( Hom ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		prstcnid.c	⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
2		prstcnid.k	⊢ ( 𝜑 → 𝐾 ∈ Proset )
3		prstchomval.l	⊢ ( 𝜑 → ≤ = ( le ‘ 𝐶 ) )
4		homid	⊢ Hom = Slot ( Hom ‘ ndx )
5		slotsbhcdif	⊢ ( ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) ∧ ( Base ‘ ndx ) ≠ ( comp ‘ ndx ) ∧ ( Hom ‘ ndx ) ≠ ( comp ‘ ndx ) )
6	5	simp3i	⊢ ( Hom ‘ ndx ) ≠ ( comp ‘ ndx )
7	1 2 4 6	prstcnidlem	⊢ ( 𝜑 → ( Hom ‘ 𝐶 ) = ( Hom ‘ ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) ) )
8		fvex	⊢ ( le ‘ 𝐾 ) ∈ V
9		snex	⊢ { 1o } ∈ V
10	8 9	xpex	⊢ ( ( le ‘ 𝐾 ) × { 1o } ) ∈ V
11	4	setsid	⊢ ( ( 𝐾 ∈ Proset ∧ ( ( le ‘ 𝐾 ) × { 1o } ) ∈ V ) → ( ( le ‘ 𝐾 ) × { 1o } ) = ( Hom ‘ ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) ) )
12	2 10 11	sylancl	⊢ ( 𝜑 → ( ( le ‘ 𝐾 ) × { 1o } ) = ( Hom ‘ ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) ) )
13		eqidd	⊢ ( 𝜑 → ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) )
14	1 2 13	prstcleval	⊢ ( 𝜑 → ( le ‘ 𝐾 ) = ( le ‘ 𝐶 ) )
15	14 3	eqtr4d	⊢ ( 𝜑 → ( le ‘ 𝐾 ) = ≤ )
16	15	xpeq1d	⊢ ( 𝜑 → ( ( le ‘ 𝐾 ) × { 1o } ) = ( ≤ × { 1o } ) )
17	7 12 16	3eqtr2rd	⊢ ( 𝜑 → ( ≤ × { 1o } ) = ( Hom ‘ 𝐶 ) )