prstcnidlem

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

	Ref	Expression
Hypotheses	prstcnid.c	No typesetting found for \|- ( ph -> C = ( ProsetToCat ` K ) ) with typecode \|-
	prstcnid.k	$⊢ φ \to K \in Proset$
	prstcnid.e	$⊢ E = Slot E (ndx)$
	prstcnid.no	$⊢ E (ndx) \neq comp (ndx)$
Assertion	prstcnidlem	$⊢ φ \to E (C) = E (K sSet ⟨Hom (ndx), \leq_{K} \times \{1_{𝑜}\}⟩)$

Step	Hyp	Ref	Expression
1		prstcnid.c	Could not format ( ph -> C = ( ProsetToCat ` K ) ) : No typesetting found for \|- ( ph -> C = ( ProsetToCat ` K ) ) with typecode \|-
2		prstcnid.k	$⊢ φ \to K \in Proset$
3		prstcnid.e	$⊢ E = Slot E (ndx)$
4		prstcnid.no	$⊢ E (ndx) \neq comp (ndx)$
5	1 2	prstcval	$⊢ φ \to C = (K sSet ⟨Hom (ndx), \leq_{K} \times \{1_{𝑜}\}⟩) sSet ⟨comp (ndx), \emptyset⟩$
6	5	fveq2d	$⊢ φ \to E (C) = E ((K sSet ⟨Hom (ndx), \leq_{K} \times \{1_{𝑜}\}⟩) sSet ⟨comp (ndx), \emptyset⟩)$
7	3 4	setsnid	$⊢ E (K sSet ⟨Hom (ndx), \leq_{K} \times \{1_{𝑜}\}⟩) = E ((K sSet ⟨Hom (ndx), \leq_{K} \times \{1_{𝑜}\}⟩) sSet ⟨comp (ndx), \emptyset⟩)$
8	6 7	eqtr4di	$⊢ φ \to E (C) = E (K sSet ⟨Hom (ndx), \leq_{K} \times \{1_{𝑜}\}⟩)$

Metamath Proof Explorer