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 ⊢ φ → C = ProsetToCat ⁡ K
prstcnid.k ⊢ φ → K ∈ Proset
Assertion prstcval ⊢ φ → C = K sSet Hom ⁡ ndx ≤ K × 1 𝑜 sSet comp ⁡ ndx ∅

Proof

Step Hyp Ref Expression
1 prstcnid.c ⊢ φ → C = ProsetToCat ⁡ K
2 prstcnid.k ⊢ φ → K ∈ Proset
3 id ⊢ k = K → k = K
4 fveq2 ⊢ k = K → ≤ k = ≤ K
5 4 xpeq1d ⊢ k = K → ≤ k × 1 𝑜 = ≤ K × 1 𝑜
6 5 opeq2d ⊢ k = K → Hom ⁡ ndx ≤ k × 1 𝑜 = Hom ⁡ ndx ≤ K × 1 𝑜
7 3 6 oveq12d ⊢ k = K → k sSet Hom ⁡ ndx ≤ k × 1 𝑜 = K sSet Hom ⁡ ndx ≤ K × 1 𝑜
8 7 oveq1d ⊢ k = K → k sSet Hom ⁡ ndx ≤ k × 1 𝑜 sSet comp ⁡ ndx ∅ = K sSet Hom ⁡ ndx ≤ K × 1 𝑜 sSet comp ⁡ ndx ∅
9 df-prstc ⊢ ProsetToCat = k ∈ Proset ⟼ k sSet Hom ⁡ ndx ≤ k × 1 𝑜 sSet comp ⁡ ndx ∅
10 ovex ⊢ K sSet Hom ⁡ ndx ≤ K × 1 𝑜 sSet comp ⁡ ndx ∅ ∈ V
11 8 9 10 fvmpt ⊢ K ∈ Proset → ProsetToCat ⁡ K = K sSet Hom ⁡ ndx ≤ K × 1 𝑜 sSet comp ⁡ ndx ∅
12 2 11 syl ⊢ φ → ProsetToCat ⁡ K = K sSet Hom ⁡ ndx ≤ K × 1 𝑜 sSet comp ⁡ ndx ∅
13 1 12 eqtrd ⊢ φ → C = K sSet Hom ⁡ ndx ≤ K × 1 𝑜 sSet comp ⁡ ndx ∅