Theorem prstcoc

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

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

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	1 2 3	prstcocval	|- ( ph -> ._|_ = ( oc ` C ) )
5	4	fveq1d	|- ( ph -> ( ._|_ ` X ) = ( ( oc ` C ) ` X ) )