This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prstcoc

Description: Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024)

Ref Expression
Hypotheses prstcnid.c ⊢ φ → C = ProsetToCat ⁡ K
prstcnid.k ⊢ φ → K ∈ Proset
prstcoc.oc ⊢ φ → ⊥ ˙ = oc ⁡ K
Assertion prstcoc ⊢ φ → ⊥ ˙ ⁡ X = oc ⁡ C ⁡ X

Proof

Step Hyp Ref Expression
1 prstcnid.c ⊢ φ → C = ProsetToCat ⁡ K
2 prstcnid.k ⊢ φ → K ∈ Proset
3 prstcoc.oc ⊢ φ → ⊥ ˙ = oc ⁡ K
4 1 2 3 prstcocval ⊢ φ → ⊥ ˙ = oc ⁡ C
5 4 fveq1d ⊢ φ → ⊥ ˙ ⁡ X = oc ⁡ C ⁡ X