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

Metamath Proof Explorer

Theorem prstcnid

Description: Components other than Hom and comp are unchanged. (Contributed by Zhi Wang, 20-Sep-2024)

Ref Expression
Hypotheses prstcnid.c ⊢ φ → C = ProsetToCat ⁡ K
prstcnid.k ⊢ φ → K ∈ Proset
prstcnid.e ⊢ E = Slot E ⁡ ndx
prstcnid.no ⊢ E ⁡ ndx ≠ comp ⁡ ndx
prstcnid.nh ⊢ E ⁡ ndx ≠ Hom ⁡ ndx
Assertion prstcnid ⊢ φ → E ⁡ K = E ⁡ C

Proof

Step Hyp Ref Expression
1 prstcnid.c ⊢ φ → C = ProsetToCat ⁡ K
2 prstcnid.k ⊢ φ → K ∈ Proset
3 prstcnid.e ⊢ E = Slot E ⁡ ndx
4 prstcnid.no ⊢ E ⁡ ndx ≠ comp ⁡ ndx
5 prstcnid.nh ⊢ E ⁡ ndx ≠ Hom ⁡ ndx
6 3 5 setsnid ⊢ E ⁡ K = E ⁡ K sSet Hom ⁡ ndx ≤ K × 1 𝑜
7 1 2 3 4 prstcnidlem ⊢ φ → E ⁡ C = E ⁡ K sSet Hom ⁡ ndx ≤ K × 1 𝑜
8 6 7 eqtr4id ⊢ φ → E ⁡ K = E ⁡ C