Metamath Proof Explorer


Theorem prstcbas

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

Ref Expression
Hypotheses prstcnid.c No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |-
prstcnid.k φKProset
prstcbas.b φB=BaseK
Assertion prstcbas φB=BaseC

Proof

Step Hyp Ref Expression
1 prstcnid.c Could not format ( ph -> C = ( ProsetToCat ` K ) ) : No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |-
2 prstcnid.k φKProset
3 prstcbas.b φB=BaseK
4 baseid Base=SlotBasendx
5 slotsbhcdif BasendxHomndxBasendxcompndxHomndxcompndx
6 5 simp2i Basendxcompndx
7 5 simp1i BasendxHomndx
8 1 2 4 6 7 prstcnid φBaseK=BaseC
9 3 8 eqtrd φB=BaseC