Theorem prstcocval

Description: Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024) (Proof shortened by AV, 12-Nov-2024)

	Ref	Expression
Hypotheses	prstcnid.c	|- ( ph -> C = ( ProsetToCat ` K ) )
	prstcnid.k	|- ( ph -> K e. Proset )
	prstcoc.oc	|- ( ph -> ._|_ = ( oc ` K ) )
Assertion	prstcocval	|- ( ph -> ._|_ = ( oc ` C ) )

Proof

Step	Hyp	Ref	Expression
1		prstcnid.c	|- ( ph -> C = ( ProsetToCat ` K ) )
2		prstcnid.k	|- ( ph -> K e. Proset )
3		prstcoc.oc	|- ( ph -> ._|_ = ( oc ` K ) )
4		ocid	|- oc = Slot ( oc ` ndx )
5		slotsdifocndx	|- ( ( oc ` ndx ) =/= ( comp ` ndx ) /\ ( oc ` ndx ) =/= ( Hom ` ndx ) )
6	5	simpli	|- ( oc ` ndx ) =/= ( comp ` ndx )
7	5	simpri	|- ( oc ` ndx ) =/= ( Hom ` ndx )
8	1 2 4 6 7	prstcnid	|- ( ph -> ( oc ` K ) = ( oc ` C ) )
9	3 8	eqtrd	|- ( ph -> ._|_ = ( oc ` C ) )