Metamath Proof Explorer
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 |
|
|
|
prstcoc.oc |
|
|
Assertion |
prstcocval |
|
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 |
|
3 |
|
prstcoc.oc |
|
4 |
|
ocid |
|
5 |
|
slotsdifocndx |
|
6 |
5
|
simpli |
|
7 |
5
|
simpri |
|
8 |
1 2 4 6 7
|
prstcnid |
|
9 |
3 8
|
eqtrd |
|