This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) , ∅ ⟩ ) )