Theorem prstcocval

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	prstcocval	$$⊢\phi \to \underset{\dot{}}{\perp }=\mathrm{oc}\left(C\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		ocid	$$⊢\mathrm{oc}=\mathrm{Slot}\mathrm{oc}\left(\mathrm{ndx}\right)$$
5		1nn0	$$⊢1\in {\mathbb{N}}_0$$
6	5 5	deccl	$$⊢11\in {\mathbb{N}}_0$$
7	6	nn0rei	$$⊢11\in ℝ$$
8		5nn	$$⊢5\in \mathbb{N}$$
9		1lt5	$$⊢1<5$$
10	5 5 8 9	declt	$$⊢11<15$$
11	7 10	ltneii	$$⊢11\ne 15$$
12		ocndx	$$⊢\mathrm{oc}\left(\mathrm{ndx}\right)=11$$
13		ccondx	$$⊢\mathrm{comp}\left(\mathrm{ndx}\right)=15$$
14	12 13	neeq12i	$$⊢\mathrm{oc}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)\leftrightarrow 11\ne 15$$
15	11 14	mpbir	$$⊢\mathrm{oc}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)$$
16		4nn	$$⊢4\in \mathbb{N}$$
17		1lt4	$$⊢1<4$$
18	5 5 16 17	declt	$$⊢11<14$$
19	7 18	ltneii	$$⊢11\ne 14$$
20		homndx	$$⊢\mathrm{Hom}\left(\mathrm{ndx}\right)=14$$
21	12 20	neeq12i	$$⊢\mathrm{oc}\left(\mathrm{ndx}\right)\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\leftrightarrow 11\ne 14$$
22	19 21	mpbir	$$⊢\mathrm{oc}\left(\mathrm{ndx}\right)\ne \mathrm{Hom}\left(\mathrm{ndx}\right)$$
23	1 2 4 15 22	prstcnid	$$⊢\phi \to \mathrm{oc}\left(K\right)=\mathrm{oc}\left(C\right)$$
24	3 23	eqtrd	$$⊢\phi \to \underset{\dot{}}{\perp }=\mathrm{oc}\left(C\right)$$