prstcval

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

	Ref	Expression
Hypotheses	prstcnid.c	$⊢ φ \to C = ProsetToCat (K)$
	prstcnid.k	$⊢ φ \to K \in Proset$
Assertion	prstcval	$⊢ φ \to C = (K sSet ⟨Hom (ndx), \leq_{K} \times \{1_{𝑜}\}⟩) sSet ⟨comp (ndx), \emptyset⟩$

Step	Hyp	Ref	Expression
1		prstcnid.c	$⊢ φ \to C = ProsetToCat (K)$
2		prstcnid.k	$⊢ φ \to K \in Proset$
3		id	$⊢ k = K \to k = K$
4		fveq2	$⊢ k = K \to \leq_{k} = \leq_{K}$
5	4	xpeq1d	$⊢ k = K \to \leq_{k} \times \{1_{𝑜}\} = \leq_{K} \times \{1_{𝑜}\}$
6	5	opeq2d	$⊢ k = K \to ⟨Hom (ndx), \leq_{k} \times \{1_{𝑜}\}⟩ = ⟨Hom (ndx), \leq_{K} \times \{1_{𝑜}\}⟩$
7	3 6	oveq12d	$⊢ k = K \to k sSet ⟨Hom (ndx), \leq_{k} \times \{1_{𝑜}\}⟩ = K sSet ⟨Hom (ndx), \leq_{K} \times \{1_{𝑜}\}⟩$
8	7	oveq1d	$⊢ k = K \to (k sSet ⟨Hom (ndx), \leq_{k} \times \{1_{𝑜}\}⟩) sSet ⟨comp (ndx), \emptyset⟩ = (K sSet ⟨Hom (ndx), \leq_{K} \times \{1_{𝑜}\}⟩) sSet ⟨comp (ndx), \emptyset⟩$
9		df-prstc	$⊢ ProsetToCat = (k \in Proset ⟼ (k sSet ⟨Hom (ndx), \leq_{k} \times \{1_{𝑜}\}⟩) sSet ⟨comp (ndx), \emptyset⟩)$
10		ovex	$⊢ (K sSet ⟨Hom (ndx), \leq_{K} \times \{1_{𝑜}\}⟩) sSet ⟨comp (ndx), \emptyset⟩ \in V$
11	8 9 10	fvmpt	$⊢ K \in Proset \to ProsetToCat (K) = (K sSet ⟨Hom (ndx), \leq_{K} \times \{1_{𝑜}\}⟩) sSet ⟨comp (ndx), \emptyset⟩$
12	2 11	syl	$⊢ φ \to ProsetToCat (K) = (K sSet ⟨Hom (ndx), \leq_{K} \times \{1_{𝑜}\}⟩) sSet ⟨comp (ndx), \emptyset⟩$
13	1 12	eqtrd	$⊢ φ \to C = (K sSet ⟨Hom (ndx), \leq_{K} \times \{1_{𝑜}\}⟩) sSet ⟨comp (ndx), \emptyset⟩$

Metamath Proof Explorer