Metamath Proof Explorer


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 φKProset
prstcoc.oc φ˙=ocK
Assertion prstcoc φ˙X=ocCX

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 φKProset
3 prstcoc.oc φ˙=ocK
4 1 2 3 prstcocval φ˙=ocC
5 4 fveq1d φ˙X=ocCX