Description: Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024) (Proof shortened by AV, 12-Nov-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | prstcnid.c | ⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) ) | |
| prstcnid.k | ⊢ ( 𝜑 → 𝐾 ∈ Proset ) | ||
| prstcoc.oc | ⊢ ( 𝜑 → ⊥ = ( oc ‘ 𝐾 ) ) | ||
| Assertion | prstcocval | ⊢ ( 𝜑 → ⊥ = ( oc ‘ 𝐶 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | prstcnid.c | ⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) ) | |
| 2 | prstcnid.k | ⊢ ( 𝜑 → 𝐾 ∈ Proset ) | |
| 3 | prstcoc.oc | ⊢ ( 𝜑 → ⊥ = ( oc ‘ 𝐾 ) ) | |
| 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 ‘ 𝐾 ) = ( oc ‘ 𝐶 ) ) |
| 9 | 3 8 | eqtrd | ⊢ ( 𝜑 → ⊥ = ( oc ‘ 𝐶 ) ) |