Theorem prstcoc

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

	Ref	Expression
Hypotheses	prstcnid.c	$$⊢\phi \to C=\mathrm{ProsetToCat}\left(K\right)$$
	prstcnid.k	$$⊢\phi \to K\in \mathrm{Proset}$$
	prstcoc.oc	$$⊢\phi \to \underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
Assertion	prstcoc	$$⊢\phi \to \underset{\dot{}}{\perp }\left(X\right)=\mathrm{oc}\left(C\right)\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		prstcnid.c	$$⊢\phi \to C=\mathrm{ProsetToCat}\left(K\right)$$
2		prstcnid.k	$$⊢\phi \to K\in \mathrm{Proset}$$
3		prstcoc.oc	$$⊢\phi \to \underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
4	1 2 3	prstcocval	$$⊢\phi \to \underset{\dot{}}{\perp }=\mathrm{oc}\left(C\right)$$
5	4	fveq1d	$$⊢\phi \to \underset{\dot{}}{\perp }\left(X\right)=\mathrm{oc}\left(C\right)\left(X\right)$$