Theorem prstcoc

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

	Ref	Expression
Hypotheses	prstcnid.c	No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |-
	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	Could not format ( ph -> C = ( ProsetToCat ` K ) ) : No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |-
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)$$