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

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 ⊢ φ → C = ProsetToCat ⁡ K
prstcnid.k ⊢ φ → K ∈ Proset
prstcoc.oc ⊢ φ → ⊥ ˙ = oc ⁡ K
Assertion prstcocval ⊢ φ → ⊥ ˙ = oc ⁡ C

Proof

Step Hyp Ref Expression
1 prstcnid.c ⊢ φ → C = ProsetToCat ⁡ K
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