Theorem prstcnidlem

Description: Lemma for prstcnid and prstchomval . (Contributed by Zhi Wang, 20-Sep-2024) (New usage is discouraged.)

	Ref	Expression
Hypotheses	prstcnid.c	⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
	prstcnid.k	⊢ ( 𝜑 → 𝐾 ∈ Proset )
	prstcnid.e	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
	prstcnid.no	⊢ ( 𝐸 ‘ ndx ) ≠ ( comp ‘ ndx )
Assertion	prstcnidlem	⊢ ( 𝜑 → ( 𝐸 ‘ 𝐶 ) = ( 𝐸 ‘ ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) ) )

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	1 2	prstcval	⊢ ( 𝜑 → 𝐶 = ( ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ∅ ⟩ ) )
6	5	fveq2d	⊢ ( 𝜑 → ( 𝐸 ‘ 𝐶 ) = ( 𝐸 ‘ ( ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ∅ ⟩ ) ) )
7	3 4	setsnid	⊢ ( 𝐸 ‘ ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) ) = ( 𝐸 ‘ ( ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ∅ ⟩ ) )
8	6 7	eqtr4di	⊢ ( 𝜑 → ( 𝐸 ‘ 𝐶 ) = ( 𝐸 ‘ ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) ) )