Theorem prstcbas

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

	Ref	Expression
Hypotheses	prstcnid.c	⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
	prstcnid.k	⊢ ( 𝜑 → 𝐾 ∈ Proset )
	prstcbas.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
Assertion	prstcbas	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		prstcnid.c	⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
2		prstcnid.k	⊢ ( 𝜑 → 𝐾 ∈ Proset )
3		prstcbas.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
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 ‘ 𝐾 ) = ( Base ‘ 𝐶 ) )
9	3 8	eqtrd	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )