Theorem prstcocval

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	prstcocval	|- ( ph -> ._|_ = ( oc ` C ) )

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		ocid	|- oc = Slot ( oc ` ndx )
5		1nn0	|- 1 e. NN0
6	5 5	deccl	|- ; 1 1 e. NN0
7	6	nn0rei	|- ; 1 1 e. RR
8		5nn	|- 5 e. NN
9		1lt5	|- 1 < 5
10	5 5 8 9	declt	|- ; 1 1 < ; 1 5
11	7 10	ltneii	|- ; 1 1 =/= ; 1 5
12		ocndx	|- ( oc ` ndx ) = ; 1 1
13		ccondx	|- ( comp ` ndx ) = ; 1 5
14	12 13	neeq12i	|- ( ( oc ` ndx ) =/= ( comp ` ndx ) <-> ; 1 1 =/= ; 1 5 )
15	11 14	mpbir	|- ( oc ` ndx ) =/= ( comp ` ndx )
16		4nn	|- 4 e. NN
17		1lt4	|- 1 < 4
18	5 5 16 17	declt	|- ; 1 1 < ; 1 4
19	7 18	ltneii	|- ; 1 1 =/= ; 1 4
20		homndx	|- ( Hom ` ndx ) = ; 1 4
21	12 20	neeq12i	|- ( ( oc ` ndx ) =/= ( Hom ` ndx ) <-> ; 1 1 =/= ; 1 4 )
22	19 21	mpbir	|- ( oc ` ndx ) =/= ( Hom ` ndx )
23	1 2 4 15 22	prstcnid	|- ( ph -> ( oc ` K ) = ( oc ` C ) )
24	3 23	eqtrd	|- ( ph -> ._|_ = ( oc ` C ) )