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	$$⊢\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	prstcocval	$$⊢\phi \to \underset{\dot{}}{\perp }=\mathrm{oc}\left(C\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		ocid	$$⊢\mathrm{oc}=\mathrm{Slot}\mathrm{oc}\left(\mathrm{ndx}\right)$$
5		slotsdifocndx	$$⊢\left(\mathrm{oc}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)\wedge \mathrm{oc}\left(\mathrm{ndx}\right)\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\right)$$
6	5	simpli	$$⊢\mathrm{oc}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)$$
7	5	simpri	$$⊢\mathrm{oc}\left(\mathrm{ndx}\right)\ne \mathrm{Hom}\left(\mathrm{ndx}\right)$$
8	1 2 4 6 7	prstcnid	$$⊢\phi \to \mathrm{oc}\left(K\right)=\mathrm{oc}\left(C\right)$$
9	3 8	eqtrd	$$⊢\phi \to \underset{\dot{}}{\perp }=\mathrm{oc}\left(C\right)$$