Metamath Proof Explorer


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 No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |-
prstcnid.k φ K Proset
prstcoc.oc φ ˙ = oc K
Assertion prstcocval φ ˙ = oc C

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 φ K Proset
3 prstcoc.oc φ ˙ = oc K
4 ocid oc = Slot oc ndx
5 slotsdifocndx oc ndx comp ndx oc ndx Hom ndx
6 5 simpli oc ndx comp ndx
7 5 simpri oc ndx Hom ndx
8 1 2 4 6 7 prstcnid φ oc K = oc C
9 3 8 eqtrd φ ˙ = oc C