Theorem prstcval

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

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

Proof

Step	Hyp	Ref	Expression
1		prstcnid.c	⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
2		prstcnid.k	⊢ ( 𝜑 → 𝐾 ∈ Proset )
3		id	⊢ ( 𝑘 = 𝐾 → 𝑘 = 𝐾 )
4		fveq2	⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ( le ‘ 𝐾 ) )
5	4	xpeq1d	⊢ ( 𝑘 = 𝐾 → ( ( le ‘ 𝑘 ) × { 1o } ) = ( ( le ‘ 𝐾 ) × { 1o } ) )
6	5	opeq2d	⊢ ( 𝑘 = 𝐾 → ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝑘 ) × { 1o } ) ⟩ = ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ )
7	3 6	oveq12d	⊢ ( 𝑘 = 𝐾 → ( 𝑘 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝑘 ) × { 1o } ) ⟩ ) = ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) )
8	7	oveq1d	⊢ ( 𝑘 = 𝐾 → ( ( 𝑘 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝑘 ) × { 1o } ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ∅ ⟩ ) = ( ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ∅ ⟩ ) )
9		df-prstc	⊢ ProsetToCat = ( 𝑘 ∈ Proset ↦ ( ( 𝑘 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝑘 ) × { 1o } ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ∅ ⟩ ) )
10		ovex	⊢ ( ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ∅ ⟩ ) ∈ V
11	8 9 10	fvmpt	⊢ ( 𝐾 ∈ Proset → ( ProsetToCat ‘ 𝐾 ) = ( ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ∅ ⟩ ) )
12	2 11	syl	⊢ ( 𝜑 → ( ProsetToCat ‘ 𝐾 ) = ( ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ∅ ⟩ ) )
13	1 12	eqtrd	⊢ ( 𝜑 → 𝐶 = ( ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ∅ ⟩ ) )