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 
|- ( ph -> C = ( ProsetToCat ` K ) )
prstcnid.k 
|- ( ph -> K e. Proset )
prstcbas.b 
|- ( ph -> B = ( Base ` K ) )
Assertion prstcbas 
|- ( ph -> B = ( Base ` C ) )

Proof

Step Hyp Ref Expression
1 prstcnid.c 
 |-  ( ph -> C = ( ProsetToCat ` K ) )
2 prstcnid.k 
 |-  ( ph -> K e. Proset )
3 prstcbas.b 
 |-  ( ph -> 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 
 |-  ( ph -> ( Base ` K ) = ( Base ` C ) )
9 3 8 eqtrd 
 |-  ( ph -> B = ( Base ` C ) )