Theorem prstcnid

Description: Components other than Hom and comp are unchanged. (Contributed by Zhi Wang, 20-Sep-2024)

	Ref	Expression
Hypotheses	prstcnid.c	⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
	prstcnid.k	⊢ ( 𝜑 → 𝐾 ∈ Proset )
	prstcnid.e	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
	prstcnid.no	⊢ ( 𝐸 ‘ ndx ) ≠ ( comp ‘ ndx )
	prstcnid.nh	⊢ ( 𝐸 ‘ ndx ) ≠ ( Hom ‘ ndx )
Assertion	prstcnid	⊢ ( 𝜑 → ( 𝐸 ‘ 𝐾 ) = ( 𝐸 ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		prstcnid.c	⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
2		prstcnid.k	⊢ ( 𝜑 → 𝐾 ∈ Proset )
3		prstcnid.e	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
4		prstcnid.no	⊢ ( 𝐸 ‘ ndx ) ≠ ( comp ‘ ndx )
5		prstcnid.nh	⊢ ( 𝐸 ‘ ndx ) ≠ ( Hom ‘ ndx )
6	3 5	setsnid	⊢ ( 𝐸 ‘ 𝐾 ) = ( 𝐸 ‘ ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) )
7	1 2 3 4	prstcnidlem	⊢ ( 𝜑 → ( 𝐸 ‘ 𝐶 ) = ( 𝐸 ‘ ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) ) )
8	6 7	eqtr4id	⊢ ( 𝜑 → ( 𝐸 ‘ 𝐾 ) = ( 𝐸 ‘ 𝐶 ) )