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

Metamath Proof Explorer

Theorem prstcbas

Description: The base set is unchanged. (Contributed by Zhi Wang, 20-Sep-2024)

Ref Expression
Hypotheses prstcnid.c ⊢ φ → C = ProsetToCat ⁡ K
prstcnid.k ⊢ φ → K ∈ Proset
prstcbas.b ⊢ φ → B = Base K
Assertion prstcbas ⊢ φ → B = Base C

Proof

Step Hyp Ref Expression
1 prstcnid.c ⊢ φ → C = ProsetToCat ⁡ K
2 prstcnid.k ⊢ φ → K ∈ Proset
3 prstcbas.b ⊢ φ → B = Base K
4 baseid ⊢ Base = Slot Base ndx
5 slotsbhcdif ⊢ Base ndx ≠ Hom ⁡ ndx ∧ Base ndx ≠ comp ⁡ ndx ∧ Hom ⁡ ndx ≠ comp ⁡ ndx
6 5 simp2i ⊢ Base ndx ≠ comp ⁡ ndx
7 5 simp1i ⊢ Base ndx ≠ Hom ⁡ ndx
8 1 2 4 6 7 prstcnid ⊢ φ → Base K = Base C
9 3 8 eqtrd ⊢ φ → B = Base C